partial commit in static_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 963893a24aef7195bd4b776d563423921d3578b7..e36bc6729a3973a630ef35609dbab14eac26960a 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,15 +19,15 @@ 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+â¦\83Tâ¦\84 ≘ f2 →
-      â\88\80f1,L1. â¦\83L1,f1â¦\84 â«\83ð\9d\90\85+ â¦\83L2,f2â¦\84 â\86\92 L1 â\8a¢ ð\9d\90\85+â¦\83Tâ¦\84 ≘ 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
   elim (lsubf_inv_atom2 … H) -H #Hg1 #H destruct
-  elim (eq_inv_pushs_dx … Hg1) -Hg1 #g #Hg #H destruct
+  elim (pr_eq_inv_pushs_dx … Hg1) -Hg1 #g #Hg #H destruct
   elim (eq_inv_xn … Hg) -Hg
-  /3 width=3 by frees_atom, isid_eq_repl_fwd/
+  /3 width=3 by frees_atom, pr_isi_eq_repl_fwd/
 | #f2 #I #K2 #W #_ #IH #g1 #Y1 #H elim (lsubf_inv_pair2 … H) -H *
   [ #f1 #K1 #H12 #H1 #H2 destruct /3 width=1 by frees_pair/
   | #f #f0 #f1 #K1 #V #H12 #Hf #Hf1 #H1 #H2 #H3 destruct
@@ -37,7 +37,7 @@ lemma lsubf_frees_trans:
   [ #f1 #L1 #H12 #H1 #H2 destruct
     /3 width=5 by lsubf_fwd_isid_dx, frees_unit/
   | #f #f0 #f1 #J #L1 #V #H12 #Hf #Hf1 #H1 #H2 destruct
-    /5 width=9 by lsubf_fwd_isid_dx, frees_eq_repl_back, frees_pair, sor_isid_inv_sn/
+    /5 width=9 by lsubf_fwd_isid_dx, frees_eq_repl_back, frees_pair, pr_sor_inv_isi_sn/
   ]
 | #f2 #I #L2 #i #_ #IH #g1 #L1 #H elim (lsubf_inv_push2 … H) -H
   /3 width=1 by frees_lref/