-lemma feqx_fqus_trans: ∀b,G1,G,L1,L,T1,T. ⦃G1,L1,T1⦄ ≛ ⦃G,L,T⦄ →
- ∀G2,L2,T2. ⦃G,L,T⦄ ⬂*[b] ⦃G2,L2,T2⦄ →
- ∃∃G,L0,T0. ⦃G1,L1,T1⦄ ⬂*[b] ⦃G,L0,T0⦄ & ⦃G,L0,T0⦄ ≛ ⦃G2,L2,T2⦄.
+lemma feqx_fqus_trans (b):
+ ∀G1,G,L1,L,T1,T. ❪G1,L1,T1❫ ≛ ❪G,L,T❫ →
+ ∀G2,L2,T2. ❪G,L,T❫ ⬂*[b] ❪G2,L2,T2❫ →
+ ∃∃G,L0,T0. ❪G1,L1,T1❫ ⬂*[b] ❪G,L0,T0❫ & ❪G,L0,T0❫ ≛ ❪G2,L2,T2❫.