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=91f7bf16f334cd6f27a70961a16c8764a61259ce;hb=fed8c1a61273b0eb4a719fda70e2b5dd31933c8a;hp=10e8a919a15790702797381358b4797a7a5ae7c2;hpb=670ad7822d59e598a38d9037d482d3de188b170c;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 10e8a919a..91f7bf16f 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
@@ -77,10 +77,6 @@ lemma lleq_inv_S: ∀L1,L2,T,l. L1 ≡[T, l+1] L2 →
                   K1 ≡[V, 0] K2 → L1 ≡[T, l] L2.
 /2 width=9 by llpx_sn_inv_S/ qed-.
 
-lemma lleq_inv_bind_O: ∀a,I,L1,L2,V,T. L1 ≡[ⓑ{a,I}V.T, 0] L2 →
-                       L1 ≡[V, 0] L2 ∧ L1.ⓑ{I}V ≡[T, 0] L2.ⓑ{I}V.
-/2 width=2 by llpx_sn_inv_bind_O/ qed-.
-
 (* Advanced forward lemmas **************************************************)
 
 lemma lleq_fwd_lref_dx: ∀L1,L2,l,i. L1 ≡[#i, l] L2 →
@@ -98,21 +94,3 @@ lemma lleq_fwd_lref_sn: ∀L1,L2,l,i. L1 ≡[#i, l] L2 →
 #L1 #L2 #l #i #H #I #K1 #V #HLK1 elim (llpx_sn_fwd_lref_sn … H … HLK1) -L1
 [ | * ] /3 width=3 by ex3_intro, or_intror, or_introl/
 qed-.
-
-lemma lleq_fwd_bind_O_dx: ∀a,I,L1,L2,V,T. L1 ≡[ⓑ{a,I}V.T, 0] L2 →
-                          L1.ⓑ{I}V ≡[T, 0] L2.ⓑ{I}V.
-/2 width=2 by llpx_sn_fwd_bind_O_dx/ qed-.
-
-(* Inversion lemmas on negated lazy quivalence for local environments *******)
-
-lemma nlleq_inv_bind: ∀a,I,L1,L2,V,T,l. (L1 ≡[ⓑ{a,I}V.T, l] L2 → ⊥) →
-                      (L1 ≡[V, l] L2 → ⊥) ∨ (L1.ⓑ{I}V ≡[T, ⫯l] L2.ⓑ{I}V → ⊥).
-/3 width=2 by nllpx_sn_inv_bind, eq_term_dec/ qed-.
-
-lemma nlleq_inv_flat: ∀I,L1,L2,V,T,l. (L1 ≡[ⓕ{I}V.T, l] L2 → ⊥) →
-                      (L1 ≡[V, l] L2 → ⊥) ∨ (L1 ≡[T, l] L2 → ⊥).
-/3 width=2 by nllpx_sn_inv_flat, eq_term_dec/ qed-.
-
-lemma nlleq_inv_bind_O: ∀a,I,L1,L2,V,T. (L1 ≡[ⓑ{a,I}V.T, 0] L2 → ⊥) →
-                        (L1 ≡[V, 0] L2 → ⊥) ∨ (L1.ⓑ{I}V ≡[T, 0] L2.ⓑ{I}V → ⊥).
-/3 width=2 by nllpx_sn_inv_bind_O, eq_term_dec/ qed-.