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 aa4fa9e8c76ea747cc812bf4de5492dbfb8e2371..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.
@@ -106,35 +103,6 @@ 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-.
 
-(* Properties on relocation *************************************************)
-
-lemma lleq_lift_le: ∀K1,K2,T,lt. K1 ≡[T, lt] K2 →
-                    ∀L1,L2,l,k. ⬇[Ⓕ, l, k] L1 ≡ K1 → ⬇[Ⓕ, l, k] L2 ≡ K2 →
-                    ∀U. ⬆[l, k] T ≡ U → lt ≤ l → L1 ≡[U, lt] L2.
-/3 width=10 by llpx_sn_lift_le, lift_mono/ qed-.
-
-lemma lleq_lift_ge: ∀K1,K2,T,lt. K1 ≡[T, lt] K2 →
-                    ∀L1,L2,l,k. ⬇[Ⓕ, l, k] L1 ≡ K1 → ⬇[Ⓕ, l, k] L2 ≡ K2 →
-                    ∀U. ⬆[l, k] T ≡ U → l ≤ lt → L1 ≡[U, lt+k] L2.
-/2 width=9 by llpx_sn_lift_ge/ qed-.
-
-(* Inversion lemmas on relocation *******************************************)
-
-lemma lleq_inv_lift_le: ∀L1,L2,U,lt. L1 ≡[U, lt] L2 →
-                        ∀K1,K2,l,k. ⬇[Ⓕ, l, k] L1 ≡ K1 → ⬇[Ⓕ, l, k] L2 ≡ K2 →
-                        ∀T. ⬆[l, k] T ≡ U → lt ≤ l → K1 ≡[T, lt] K2.
-/3 width=10 by llpx_sn_inv_lift_le, ex2_intro/ qed-.
-
-lemma lleq_inv_lift_be: ∀L1,L2,U,lt. L1 ≡[U, lt] L2 →
-                        ∀K1,K2,l,k. ⬇[Ⓕ, l, k] L1 ≡ K1 → ⬇[Ⓕ, l, k] L2 ≡ K2 →
-                        ∀T. ⬆[l, k] T ≡ U → l ≤ lt → lt ≤ l + k → K1 ≡[T, l] K2.
-/2 width=11 by llpx_sn_inv_lift_be/ qed-.
-
-lemma lleq_inv_lift_ge: ∀L1,L2,U,lt. L1 ≡[U, lt] L2 →
-                        ∀K1,K2,l,k. ⬇[Ⓕ, l, k] L1 ≡ K1 → ⬇[Ⓕ, l, k] L2 ≡ K2 →
-                        ∀T. ⬆[l, k] T ≡ U → l + k ≤ lt → K1 ≡[T, lt-k] K2.
-/2 width=9 by llpx_sn_inv_lift_ge/ 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 → ⊥) →