X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Flsubf_frees.ma;h=09d8339d1173929b89b6a1da621a982bbff469eb;hb=86d7622f88247d83b2c366a722d2994a4af91929;hp=700bb0bb0b53eb799054ffcb01422d56e50b4fff;hpb=b7de6afb9d3260ffea86ddf824e497419e1b56fb;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..09d8339d1 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 *************************)