(* Basic_2A1: uses: fqu_cpxs_trans_neq *)
lemma fqu_cpxs_trans_tneqx (b):
∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂[b] ❪G2,L2,T2❫ →
- â\88\80U2. â\9dªG2,L2â\9d« â\8a¢ T2 â¬\88* U2 â\86\92 (T2 â\89\9b U2 → ⊥) →
- â\88\83â\88\83U1. â\9dªG1,L1â\9d« â\8a¢ T1 â¬\88* U1 & T1 â\89\9b U1 → ⊥ & ❪G1,L1,U1❫ ⬂[b] ❪G2,L2,U2❫.
+ â\88\80U2. â\9dªG2,L2â\9d« â\8a¢ T2 â¬\88* U2 â\86\92 (T2 â\89\85 U2 → ⊥) →
+ â\88\83â\88\83U1. â\9dªG1,L1â\9d« â\8a¢ T1 â¬\88* U1 & T1 â\89\85 U1 → ⊥ & ❪G1,L1,U1❫ ⬂[b] ❪G2,L2,U2❫.
#b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
[ #I #G #L #V1 #V2 #HV12 #_ elim (lifts_total V2 𝐔❨1❩)
#U2 #HVU2 @(ex3_intro … U2)
[1,3: /3 width=7 by cpxs_delta, fqu_drop/
- | #H lapply (teqx_inv_lref1 … H) -H
+ | #H lapply (teqg_inv_lref1 … H) -H
#H destruct /2 width=5 by lifts_inv_lref2_uni_lt/
]
| #I #G #L #V1 #T #V2 #HV12 #H0 @(ex3_intro … (②[I]V2.T))
(* Basic_2A1: uses: fquq_cpxs_trans_neq *)
lemma fquq_cpxs_trans_tneqx (b):
∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂⸮[b] ❪G2,L2,T2❫ →
- â\88\80U2. â\9dªG2,L2â\9d« â\8a¢ T2 â¬\88* U2 â\86\92 (T2 â\89\9b U2 → ⊥) →
- â\88\83â\88\83U1. â\9dªG1,L1â\9d« â\8a¢ T1 â¬\88* U1 & T1 â\89\9b U1 → ⊥ & ❪G1,L1,U1❫ ⬂⸮[b] ❪G2,L2,U2❫.
+ â\88\80U2. â\9dªG2,L2â\9d« â\8a¢ T2 â¬\88* U2 â\86\92 (T2 â\89\85 U2 → ⊥) →
+ â\88\83â\88\83U1. â\9dªG1,L1â\9d« â\8a¢ T1 â¬\88* U1 & T1 â\89\85 U1 → ⊥ & ❪G1,L1,U1❫ ⬂⸮[b] ❪G2,L2,U2❫.
#b #G1 #G2 #L1 #L2 #T1 #T2 #H12 elim H12 -H12
[ #H12 #U2 #HTU2 #H elim (fqu_cpxs_trans_tneqx … H12 … HTU2 H) -T2
/3 width=4 by fqu_fquq, ex3_intro/
(* Basic_2A1: uses: fqup_cpxs_trans_neq *)
lemma fqup_cpxs_trans_tneqx (b):
∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂+[b] ❪G2,L2,T2❫ →
- â\88\80U2. â\9dªG2,L2â\9d« â\8a¢ T2 â¬\88* U2 â\86\92 (T2 â\89\9b U2 → ⊥) →
- â\88\83â\88\83U1. â\9dªG1,L1â\9d« â\8a¢ T1 â¬\88* U1 & T1 â\89\9b U1 → ⊥ & ❪G1,L1,U1❫ ⬂+[b] ❪G2,L2,U2❫.
+ â\88\80U2. â\9dªG2,L2â\9d« â\8a¢ T2 â¬\88* U2 â\86\92 (T2 â\89\85 U2 → ⊥) →
+ â\88\83â\88\83U1. â\9dªG1,L1â\9d« â\8a¢ T1 â¬\88* U1 & T1 â\89\85 U1 → ⊥ & ❪G1,L1,U1❫ ⬂+[b] ❪G2,L2,U2❫.
#b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind_dx … H) -G1 -L1 -T1
[ #G1 #L1 #T1 #H12 #U2 #HTU2 #H elim (fqu_cpxs_trans_tneqx … H12 … HTU2 H) -T2
/3 width=4 by fqu_fqup, ex3_intro/
(* Basic_2A1: uses: fqus_cpxs_trans_neq *)
lemma fqus_cpxs_trans_tneqx (b):
∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂*[b] ❪G2,L2,T2❫ →
- â\88\80U2. â\9dªG2,L2â\9d« â\8a¢ T2 â¬\88* U2 â\86\92 (T2 â\89\9b U2 → ⊥) →
- â\88\83â\88\83U1. â\9dªG1,L1â\9d« â\8a¢ T1 â¬\88* U1 & T1 â\89\9b U1 → ⊥ & ❪G1,L1,U1❫ ⬂*[b] ❪G2,L2,U2❫.
+ â\88\80U2. â\9dªG2,L2â\9d« â\8a¢ T2 â¬\88* U2 â\86\92 (T2 â\89\85 U2 → ⊥) →
+ â\88\83â\88\83U1. â\9dªG1,L1â\9d« â\8a¢ T1 â¬\88* U1 & T1 â\89\85 U1 → ⊥ & ❪G1,L1,U1❫ ⬂*[b] ❪G2,L2,U2❫.
#b #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fqus_inv_fqup … H12) -H12
[ #H12 elim (fqup_cpxs_trans_tneqx … H12 … HTU2 H) -T2
/3 width=4 by fqup_fqus, ex3_intro/