update in ground static_2 basic_2 apps_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / static / rex_rex.ma

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 e3d0aee798028727edb627f6db86e6504e38d2a5..5aaee3689b68ba54dcfb2484f9fd4d72ae1a4943 100644 (file)
--- 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 →
-      â\88\80f. L1 â\8a¢ ð\9d\90\85+â\9dªTâ\9d« ≘ f → L1 ⪤[cext2 R,cfull,f] L2.
+      â\88\80f. L1 â\8a¢ ð\9d\90\85+â\9d¨Tâ\9d© ≘ f → L1 ⪤[cext2 R,cfull,f] L2.
 #R #L1 #L2 #T * /3 width=6 by frees_mono, sex_eq_repl_back/
 qed-.