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

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops.etc
deleted file mode 100644 (file)
index 5d51b83..0000000
--- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops.etc
+++ /dev/null
@@ -1,2 +0,0 @@
-lemma drop_inv_refl: ∀L,l,m. ⬇[Ⓕ, l, m] L ≡ L → m = 0.
-/2 width=5 by drop_inv_length_eq/ qed-.