X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fetc%2Flleq%2Flleq_drop.etc;h=10e8a919a15790702797381358b4797a7a5ae7c2;hb=670ad7822d59e598a38d9037d482d3de188b170c;hp=87ceaf096c88f8d3142b99993d02c237f8373b23;hpb=7412538ab43afe9a19c5f4be369bed82b2ab6193;p=helm.git

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 87ceaf096..10e8a919a 100644
--- 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.