X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Ffeqg_fqup.ma;h=17b7c8e79aaa974db216bc25c67d813d1fd62794;hb=8ec019202bff90959cf1a7158b309e7f83fa222e;hp=e50f40818650498957b3c14895816153580321ec;hpb=b118146b97959e6a6dde18fdd014b8e1e676a2d1;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/feqg_fqup.ma b/matita/matita/contribs/lambdadelta/static_2/static/feqg_fqup.ma
index e50f40818..17b7c8e79 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/feqg_fqup.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/feqg_fqup.ma
@@ -22,7 +22,7 @@ include "static_2/static/feqg.ma".
 lemma teqg_feqg (S):
       reflexive … S →
       ∀T1,T2. T1 ≛[S] T2 →
-      ∀G,L. ❪G,L,T1❫ ≛[S] ❪G,L,T2❫.
+      ∀G,L. ❨G,L,T1❩ ≛[S] ❨G,L,T2❩.
 /3 width=1 by feqg_intro_sn, reqg_refl/ qed.
 
 (* Advanced properties ******************************************************)