- updated equivalence on referred entries: it nust be degree-based

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / etc_new / frees / frees.etc

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 (file)
index a9349e8..0000000
--- 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.