-lemma lpx_fqus_trans: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⊐*[b] ⦃G2,L2,T2⦄ →
- ∀K1. ⦃G1,K1⦄ ⊢ ⬈[h] L1 →
- ∃∃K2,T. ⦃G1,K1⦄ ⊢ T1 ⬈*[h] T & ⦃G1,K1,T⦄ ⊐*[b] ⦃G2,K2,T2⦄ & ⦃G2,K2⦄ ⊢ ⬈[h] L2.
-#h #b #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #HKL1 elim (fqus_inv_fqup … H) -H
+lemma lpx_fqus_trans (b):
+ ∀G1,G2,L1,L2,T1,T2. ❨G1,L1,T1❩ ⬂*[b] ❨G2,L2,T2❩ →
+ ∀K1. ❨G1,K1❩ ⊢ ⬈ L1 →
+ ∃∃K2,T. ❨G1,K1❩ ⊢ T1 ⬈* T & ❨G1,K1,T❩ ⬂*[b] ❨G2,K2,T2❩ & ❨G2,K2❩ ⊢ ⬈ L2.
+#b #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #HKL1 elim (fqus_inv_fqup … H) -H