-(* Note: a proof based on fqu_cpx_trans_ntdeq might exist *)
-lemma fqu_cpxs_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ →
- ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈*[h] U2 → (T2 ≡[h, o] U2 → ⊥) →
- ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] U1 & T1 ≡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐[b] ⦃G2, L2, U2⦄.
-#h #o #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❵)
+(* Note: a proof based on fqu_cpx_trans_tneqx might exist *)
+(* Basic_2A1: uses: fqu_cpxs_trans_neq *)
+lemma fqu_cpxs_trans_tneqg (S) (b):
+ ∀G1,G2,L1,L2,T1,T2. ❨G1,L1,T1❩ ⬂[b] ❨G2,L2,T2❩ →
+ ∀U2. ❨G2,L2❩ ⊢ T2 ⬈* U2 → (T2 ≛[S] U2 → ⊥) →
+ ∃∃U1. ❨G1,L1❩ ⊢ T1 ⬈* U1 & T1 ≛[S] U1 → ⊥ & ❨G1,L1,U1❩ ⬂[b] ❨G2,L2,U2❩.
+#S #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❩)