include "static_2/static/feqg.ma".
(* SORT-IRRELEVANT EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES *************)
-(*
-definition feqx: relation6 genv lenv term genv lenv term ≝
- feqg sfull.
-*)
+
interpretation
"sort-irrelevant equivalence on referred entries (closure)"
'ApproxEqSn G1 L1 T1 G2 L2 T2 = (feqg sfull G1 L1 T1 G2 L2 T2).
(* Basic_properties *********************************************************)
lemma feqg_feqx (S) (G1) (G2) (L1) (L2) (T1) (T2):
- â\9dªG1,L1,T1â\9d« â\89\9b[S] â\9dªG2,L2,T2â\9d« â\86\92 â\9dªG1,L1,T1â\9d« â\89\85 â\9dªG2,L2,T2â\9d«.
+ â\9d¨G1,L1,T1â\9d© â\89\9b[S] â\9d¨G2,L2,T2â\9d© â\86\92 â\9d¨G1,L1,T1â\9d© â\89\85 â\9d¨G2,L2,T2â\9d©.
#S #G1 #G2 #L1 #L2 #T1 #T2 #H
elim (feqg_inv_gen_sn … H) -H
/3 width=2 by feqg_intro_sn, reqg_reqx, teqg_teqx/