-lemma lpr_fquq_trans (h) (b): ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮[b] ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡[h] L1 →
- ∃∃n,K2,T. ⦃G1, K1⦄ ⊢ T1 ➡[n, h] T & ⦃G1, K1, T⦄ ⊐⸮[b] ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h] L2 & n ≤ 1.
+lemma lpr_fquq_trans (h) (b): ∀G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂⸮[b] ⦃G2,L2,T2⦄ →
+ ∀K1. ⦃G1,K1⦄ ⊢ ➡[h] L1 →
+ ∃∃n,K2,T. ⦃G1,K1⦄ ⊢ T1 ➡[n,h] T & ⦃G1,K1,T⦄ ⬂⸮[b] ⦃G2,K2,T2⦄ & ⦃G2,K2⦄ ⊢ ➡[h] L2 & n ≤ 1.