X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Frex_rex.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Frex_rex.ma;h=5aaee3689b68ba54dcfb2484f9fd4d72ae1a4943;hb=8ec019202bff90959cf1a7158b309e7f83fa222e;hp=e3d0aee798028727edb627f6db86e6504e38d2a5;hpb=33d0a7a9029859be79b25b5a495e0f30dab11f37;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/rex_rex.ma b/matita/matita/contribs/lambdadelta/static_2/static/rex_rex.ma
index e3d0aee79..5aaee3689 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/rex_rex.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/rex_rex.ma
@@ -22,7 +22,7 @@ include "static_2/static/rex.ma".
 
 lemma rex_inv_frees (R):
       ∀L1,L2,T. L1 ⪤[R,T] L2 →
-      ∀f. L1 ⊢ 𝐅+❪T❫ ≘ f → L1 ⪤[cext2 R,cfull,f] L2.
+      ∀f. L1 ⊢ 𝐅+❨T❩ ≘ f → L1 ⪤[cext2 R,cfull,f] L2.
 #R #L1 #L2 #T * /3 width=6 by frees_mono, sex_eq_repl_back/
 qed-.