X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fetc_new%2Ffrees%2Ffrees.etc;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fetc_new%2Ffrees%2Ffrees.etc;h=0000000000000000000000000000000000000000;hb=b4b5f03ffca4f250a1dc02f277b70e4f33ac8a9b;hp=a9349e87022006b1240cb305af0850b0add9b281;hpb=09b4420070d6a71990e16211e499b51dbb0742cb;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees.etc
deleted file mode 100644
index a9349e870..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees.etc
+++ /dev/null
@@ -1,5 +0,0 @@
-(* A Basic_A2 lemma we do not need so far *)
-axiom frees_pair_flat: ∀L,T,f1,I1,V1. L.ⓑ{I1}V1 ⊢ 𝐅*⦃T⦄ ≡ f1 →
-                       ∀f2,I2,V2. L.ⓑ{I2}V2 ⊢ 𝐅*⦃T⦄ ≡ f2 →
-                       ∀f0. f1 ⋓ f2 ≡ f0 →
-                       ∀I0,I. L.ⓑ{I0}ⓕ{I}V1.V2 ⊢ 𝐅*⦃T⦄ ≡ f0.