+@(cpx_teqg_repl_reqg … HT2)
+/2 width=7 by reqg_sym, teqg_sym, teqg_refl/
+qed-.
+
+lemma feqg_cpx_trans_feqg (S):
+ reflexive … S → symmetric … S →
+ ∀G1,G2,L1,L2,T1,T. ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T❫ →
+ ∀T2. ❪G2,L2❫ ⊢ T ⬈ T2 → ❪G1,L1,T2❫ ≛[S] ❪G2,L2,T2❫.
+#S #H1S #H2S #G1 #G2 #L1 #L2 #T1 #T #H #T2 #HT2
+elim (feqg_inv_gen_dx … H) -H // #H #HL12 #_ destruct