X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Ffeqx_fqup.ma;h=2821e6718b56cf8217eee39f449f2d8360f8b1da;hp=2919d492bfb6d844196bfa54cf340b24da879684;hb=bd53c4e895203eb049e75434f638f26b5a161a2b;hpb=3b7b8afcb429a60d716d5226a5b6ab0d003228b1

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/feqx_fqup.ma b/matita/matita/contribs/lambdadelta/static_2/static/feqx_fqup.ma
index 2919d492b..2821e6718 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/feqx_fqup.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/feqx_fqup.ma
@@ -20,7 +20,7 @@ include "static_2/static/feqx.ma".
 (* Properties with sort-irrelevant equivalence for terms ********************)
 
 lemma teqx_feqx: ∀T1,T2. T1 ≛ T2 →
-                 ∀G,L. ⦃G,L,T1⦄ ≛ ⦃G,L,T2⦄.
+                 ∀G,L. ❪G,L,T1❫ ≛ ❪G,L,T2❫.
 /2 width=1 by feqx_intro_sn/ qed.
 
 (* Advanced properties ******************************************************)