-lemma fpbs_cpxs_tdeq_fqup_lpx_trans: ∀h,G1,G3,L1,L3,T1,T3. ⦃G1, L1, T1⦄ ≥ [h] ⦃G3, L3, T3⦄ →
- ∀T4. ⦃G3, L3⦄ ⊢ T3 ⬈*[h] T4 → ∀T5. T4 ≛ T5 →
- ∀G2,L4,T2. ⦃G3, L3, T5⦄ ⊐+ ⦃G2, L4, T2⦄ →
- ∀L2. ⦃G2, L4⦄ ⊢ ⬈[h] L2 → ⦃G1, L1, T1⦄ ≥ [h] ⦃G2, L2, T2⦄.
+lemma fpbs_cpxs_tdeq_fqup_lpx_trans: ∀h,G1,G3,L1,L3,T1,T3. ⦃G1,L1,T1⦄ ≥ [h] ⦃G3,L3,T3⦄ →
+ ∀T4. ⦃G3,L3⦄ ⊢ T3 ⬈*[h] T4 → ∀T5. T4 ≛ T5 →
+ ∀G2,L4,T2. ⦃G3,L3,T5⦄ ⊐+ ⦃G2,L4,T2⦄ →
+ ∀L2. ⦃G2,L4⦄ ⊢ ⬈[h] L2 → ⦃G1,L1,T1⦄ ≥ [h] ⦃G2,L2,T2⦄.