update in ground static_2 basic_2 apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/lsubf_frees.ma b/matita/matita/contribs/lambdadelta/static_2/static/lsubf_frees.ma
index e36bc6729a3973a630ef35609dbab14eac26960a..a96ad6db9e3174adfdafdd9abdfa39117be6226f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/static/lsubf_frees.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/lsubf_frees.ma
@@ -19,8 +19,8 @@ include "static_2/static/lsubf.ma".
 (* Properties with context-sensitive free variables *************************)
 
 lemma lsubf_frees_trans:
-      â\88\80f2,L2,T. L2 â\8a¢ ð\9d\90\85+â\9dªTâ\9d« ≘ f2 →
-      â\88\80f1,L1. â\9dªL1,f1â\9d« â«\83ð\9d\90\85+ â\9dªL2,f2â\9d« â\86\92 L1 â\8a¢ ð\9d\90\85+â\9dªTâ\9d« ≘ f1.
+      â\88\80f2,L2,T. L2 â\8a¢ ð\9d\90\85+â\9d¨Tâ\9d© ≘ f2 →
+      â\88\80f1,L1. â\9d¨L1,f1â\9d© â«\83ð\9d\90\85+ â\9d¨L2,f2â\9d© â\86\92 L1 â\8a¢ ð\9d\90\85+â\9d¨Tâ\9d© ≘ 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