renaming in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / lsubf_frees.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_frees.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_frees.ma
index b1f39c8123257c83761dc94ec69bd6291673a14a..390e6f13a368c47fb2b4b42f80506dba3f179ece 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_frees.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_frees.ma
@@ -18,8 +18,8 @@ include "basic_2/static/lsubf.ma".
 
 (* Properties with context-sensitive free variables *************************)
 
-lemma lsubf_frees_trans: â\88\80f2,L2,T. L2 â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89¡ f2 →
-                         â\88\80f1,L1. â¦\83L1, f1â¦\84 â«\83ð\9d\90\85* â¦\83L2, f2â¦\84 â\86\92 L1 â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89¡ f1.
+lemma lsubf_frees_trans: â\88\80f2,L2,T. L2 â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89\98 f2 →
+                         â\88\80f1,L1. â¦\83L1, f1â¦\84 â«\83ð\9d\90\85* â¦\83L2, f2â¦\84 â\86\92 L1 â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89\98 f1.
 #f2 #L2 #T #H elim H -f2 -L2 -T
 [ /3 width=5 by lsubf_fwd_isid_dx, frees_sort/
 | #f2 #i #Hf2 #g1 #Y1 #H