lemma teqg_feqg (S):
reflexive … S →
∀T1,T2. T1 ≛[S] T2 →
- â\88\80G,L. â\9dªG,L,T1â\9d« â\89\9b[S] â\9dªG,L,T2â\9d«.
+ â\88\80G,L. â\9d¨G,L,T1â\9d© â\89\9b[S] â\9d¨G,L,T2â\9d©.
/3 width=1 by feqg_intro_sn, reqg_refl/ qed.
(* Advanced properties ******************************************************)