X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Ffeqx.ma;h=f3388bfa437ed1299777740202a9f2a91b2d998c;hb=2e4a7c54ef77c10cb1cef4b59518c473245ea935;hp=9804e73c2aa46eb7557c41b331ac42fb72f158c3;hpb=e23331eef5817eaa6c5e1c442d1d6bbb18650573;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/feqx.ma b/matita/matita/contribs/lambdadelta/static_2/static/feqx.ma
index 9804e73c2..f3388bfa4 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/feqx.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/feqx.ma
@@ -17,10 +17,7 @@ include "static_2/static/reqx.ma".
 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).
@@ -28,7 +25,7 @@ interpretation
 (* Basic_properties *********************************************************)
 
 lemma feqg_feqx (S) (G1) (G2) (L1) (L2) (T1) (T2):
-      ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≅ ❪G2,L2,T2❫.
+      ❨G1,L1,T1❩ ≛[S] ❨G2,L2,T2❩ → ❨G1,L1,T1❩ ≅ ❨G2,L2,T2❩.
 #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/