advances on lfsx ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / etc / lleq / lleq_drop.etc

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lleq/lleq_drop.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lleq/lleq_drop.etc
index 87ceaf096c88f8d3142b99993d02c237f8373b23..10e8a919a15790702797381358b4797a7a5ae7c2 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/lleq/lleq_drop.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lleq/lleq_drop.etc
@@ -23,9 +23,6 @@ lemma lleq_bind_repl_O: ∀I,L1,L2,V,T. L1.ⓑ{I}V ≡[T, 0] L2.ⓑ{I}V →
                         ∀J,W. L1 ≡[W, 0] L2 → L1.ⓑ{J}W ≡[T, 0] L2.ⓑ{J}W.
 /2 width=7 by llpx_sn_bind_repl_O/ qed-.
 
-lemma lleq_dec: ∀T,L1,L2,l. Decidable (L1 ≡[T, l] L2).
-/3 width=1 by llpx_sn_dec, eq_term_dec/ qed-.
-
 lemma lleq_llpx_sn_trans: ∀R. lleq_transitive R →
                           ∀L1,L2,T,l. L1 ≡[T, l] L2 →
                           ∀L. llpx_sn R l T L2 L → llpx_sn R l T L1 L.