-lemma fdeq_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 fdeq_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⦄.