-lemma teqx_fquq_trans: ∀b,G1,G2,L1,L2,U1,T1. ❪G1,L1,U1❫ ⬂⸮[b] ❪G2,L2,T1❫ →
- ∀U2. U2 ≛ U1 →
- ∃∃L,T2. ❪G1,L1,U2❫ ⬂⸮[b] ❪G2,L,T2❫ & T2 ≛ T1 & L ≛[T1] L2.
+lemma teqx_fquq_trans (b):
+ ∀G1,G2,L1,L2,U1,T1. ❪G1,L1,U1❫ ⬂⸮[b] ❪G2,L2,T1❫ →
+ ∀U2. U2 ≛ U1 →
+ ∃∃L,T2. ❪G1,L1,U2❫ ⬂⸮[b] ❪G2,L,T2❫ & T2 ≛ T1 & L ≛[T1] L2.