X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Flsubf_frees.ma;h=b1f39c8123257c83761dc94ec69bd6291673a14a;hb=a5c71699f1d0cf63a769c71dd8b8cd5dfff1933d;hp=700bb0bb0b53eb799054ffcb01422d56e50b4fff;hpb=98fbba1b68d457807c73ebf70eb2a48696381da4;p=helm.git

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 700bb0bb0..b1f39c812 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_frees.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_frees.ma
@@ -14,10 +14,6 @@
 
 include "basic_2/static/lsubf.ma".
 
-axiom lsubf_inv_sor_dx: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
-                        ∀x2,y2. x2⋓y2 ≡ f2 →
-                        ∃∃x1,y1. ⦃L1, x1⦄ ⫃𝐅* ⦃L2, x2⦄ & ⦃L1, y1⦄ ⫃𝐅* ⦃L2, y2⦄ & x1⋓y1 ≡ f1.
-
 (* RESTRICTED REFINEMENT FOR CONTEXT-SENSITIVE FREE VARIABLES ***************)
 
 (* Properties with context-sensitive free variables *************************)
@@ -47,7 +43,7 @@ lemma lsubf_frees_trans: ∀f2,L2,T. L2 ⊢ 𝐅*⦃T⦄ ≡ f2 →
 | /3 width=5 by lsubf_fwd_isid_dx, frees_gref/
 | #f2V #f2T #f2 #p #I #L2 #V #T #_ #_ #Hf2 #IHV #IHT #f1 #L1 #H12
   elim (lsubf_inv_sor_dx … H12 … Hf2) -f2 #f1V #g1T #HV #HT #Hf1
-  elim (lsubf_tl_dx … (BPair I V) … HT) -HT #f1T #HT #H destruct
+  elim (lsubf_bind_tl_dx … (BPair I V) … HT) -HT #f1T #HT #H destruct
   /3 width=5 by frees_bind/
 | #f2V #f2T #f2 #I #L2 #V #T #_ #_ #Hf2 #IHV #IHT #f1 #L1 #H12
   elim (lsubf_inv_sor_dx … H12 … Hf2) -f2 /3 width=5 by frees_flat/