From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 20 Mar 2014 11:51:46 +0000 (+0000)
Subject: continuing on lazy pointwise extensions ...
X-Git-Tag: make_still_working~946
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1e414c3226307112e8289e014e2941479df7c663;p=helm.git

continuing on lazy pointwise extensions ...
---

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/lift_neg.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/lift_neg.etc
new file mode 100644
index 000000000..220748ed3
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/lift_neg.etc
@@ -0,0 +1,60 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/relocation/lift.ma".
+
+(* BASIC TERM RELOCATION ****************************************************)
+
+(* Properties on negated basic relocation ***********************************)
+
+lemma nlift_lref_be_SO: ∀X,i. ⇧[i, 1] X ≡ #i → ⊥.
+/2 width=7 by lift_inv_lref2_be/ qed-.
+
+lemma nlift_bind_sn: ∀W,d,e. (∀V. ⇧[d, e] V ≡ W → ⊥) →
+                     ∀a,I,U. (∀X. ⇧[d, e] X ≡ ⓑ{a,I}W.U → ⊥).
+#W #d #e #HW #a #I #U #X #H elim (lift_inv_bind2 … H) -H /2 width=2 by/
+qed-.
+
+lemma nlift_bind_dx: ∀U,d,e. (∀T. ⇧[d+1, e] T ≡ U → ⊥) →
+                     ∀a,I,W. (∀X. ⇧[d, e] X ≡ ⓑ{a,I}W.U → ⊥).
+#U #d #e #HU #a #I #W #X #H elim (lift_inv_bind2 … H) -H /2 width=2 by/
+qed-.
+
+lemma nlift_flat_sn: ∀W,d,e. (∀V. ⇧[d, e] V ≡ W → ⊥) →
+                     ∀I,U. (∀X. ⇧[d, e] X ≡ ⓕ{I}W.U → ⊥).
+#W #d #e #HW #I #U #X #H elim (lift_inv_flat2 … H) -H /2 width=2 by/
+qed-.
+
+lemma nlift_flat_dx: ∀U,d,e. (∀T. ⇧[d, e] T ≡ U → ⊥) →
+                     ∀I,W. (∀X. ⇧[d, e] X ≡ ⓕ{I}W.U → ⊥).
+#U #d #e #HU #I #W #X #H elim (lift_inv_flat2 … H) -H /2 width=2 by/
+qed-.
+
+(* Inversion lemmas on negated basic relocation *****************************)
+
+lemma nlift_inv_bind: ∀a,I,W,U,d,e. (∀X. ⇧[d, e] X ≡ ⓑ{a,I}W.U → ⊥) →
+                      (∀V. ⇧[d, e] V ≡ W → ⊥) ∨ (∀T. ⇧[d+1, e] T ≡ U → ⊥).
+#a #I #W #U #d #e #H elim (is_lift_dec W d e)
+[ * /4 width=2 by lift_bind, or_intror/
+| /4 width=2 by ex_intro, or_introl/
+]
+qed-.
+
+lemma nlift_inv_flat: ∀I,W,U,d,e. (∀X. ⇧[d, e] X ≡ ⓕ{I}W.U → ⊥) →
+                      (∀V. ⇧[d, e] V ≡ W → ⊥) ∨ (∀T. ⇧[d, e] T ≡ U → ⊥).
+#I #W #U #d #e #H elim (is_lift_dec W d e)
+[ * /4 width=2 by lift_flat, or_intror/
+| /4 width=2 by ex_intro, or_introl/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/lleq_alt.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/lleq_alt.etc
new file mode 100644
index 000000000..ccf131d5a
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/lleq_alt.etc
@@ -0,0 +1,41 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/relocation/llpx_sn_alt.ma".
+include "basic_2/relocation/lleq.ma".
+
+(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
+
+(* Alternative definition ***************************************************)
+
+theorem lleq_intro_alt: ∀L1,L2,T,d. |L1| = |L2| →
+                        (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
+                           ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+                           ∧∧ I1 = I2 & V1 = V2 & K1 ⋕[V1, 0] K2
+                        ) → L1 ⋕[T, d] L2.
+#L1 #L2 #T #d #HL12 #IH @llpx_sn_intro_alt // -HL12
+#I1 #I2 #K1 #K2 #HLK1 #HLK2 #i #Hid #HnT #HLK1 #HLK2
+elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /2 width=1 by and3_intro/
+qed.
+
+theorem lleq_fwd_alt: ∀L1,L2,T,d. L1 ⋕[T, d] L2 →
+                      |L1| = |L2| ∧
+                      ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
+                      ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+                      ∧∧ I1 = I2 & V1 = V2 & K1 ⋕[V1, 0] K2.
+#L1 #L2 #T #d #H elim (llpx_sn_fwd_alt … H) -H
+#HL12 #IH @conj //
+#I1 #I2 #K1 #K2 #HLK1 #HLK2 #i #Hid #HnT #HLK1 #HLK2
+elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /2 width=1 by and3_intro/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn_alt.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn_alt.etc
new file mode 100644
index 000000000..4356553ff
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn_alt.etc
@@ -0,0 +1,250 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/relocation/lift_neg.ma".
+include "basic_2/relocation/ldrop_ldrop.ma".
+include "basic_2/relocation/llpx_sn.ma".
+
+(* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
+
+(* alternative definition of llpx_sn_alt *)
+inductive llpx_sn_alt (R:relation3 lenv term term): relation4 ynat term lenv lenv ≝
+| llpx_sn_alt_intro: ∀L1,L2,T,d.
+                     (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
+                       ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → I1 = I2 ∧ R K1 V1 V2
+                     ) →
+                     (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
+                       ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → llpx_sn_alt R 0 V1 K1 K2
+                     ) → |L1| = |L2| → llpx_sn_alt R d T L1 L2
+.
+
+(* Basic forward lemmas ******************************************************)
+
+lemma llpx_sn_alt_fwd_gen: ∀R,L1,L2,T,d. llpx_sn_alt R d T L1 L2 →
+                           |L1| = |L2| ∧
+                           ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
+                           ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+                           ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn_alt R 0 V1 K1 K2.
+#R #L1 #L2 #T #d * -L1 -L2 -T -d
+#L1 #L2 #T #d #IH1 #IH2 #HL12 @conj //
+#I1 #I2 #K1 #K2 #HLK1 #HLK2 #i #Hid #HnT #HLK1 #HLK2
+elim (IH1 … HnT HLK1 HLK2) -IH1 /4 width=8 by and3_intro/
+qed-.
+
+lemma llpx_sn_alt_fwd_length: ∀R,L1,L2,T,d. llpx_sn_alt R d T L1 L2 → |L1| = |L2|.
+#R #L1 #L2 #T #d * -L1 -L2 -T -d //
+qed-.
+
+fact llpx_sn_alt_fwd_lref_aux: ∀R,L1,L2,X,d. llpx_sn_alt R d X L1 L2 → ∀i. X = #i →
+                               ∨∨ |L1| ≤ i ∧ |L2| ≤ i
+                                | yinj i < d
+                                | ∃∃I,K1,K2,V1,V2. ⇩[i] L1 ≡ K1.ⓑ{I}V1 &
+                                                   ⇩[i] L2 ≡ K2.ⓑ{I}V2 &
+                                                   llpx_sn_alt R (yinj 0) V1 K1 K2 &
+                                                   R K1 V1 V2 & d ≤ yinj i.
+#R #L1 #L2 #X #d * -L1 -L2 -X -d
+#L1 #L2 #X #d #H1X #H2X #HL12 #i #H destruct
+elim (lt_or_ge i (|L1|)) /3 width=1 by or3_intro0, conj/
+elim (ylt_split i d) /3 width=1 by or3_intro1/
+#Hdi #HL1 elim (ldrop_O1_lt … HL1) #I1 #K1 #V1 #HLK1
+elim (ldrop_O1_lt L2 i) // #I2 #K2 #V2 #HLK2
+elim (H1X … HLK1 HLK2) -H1X /2 width=3 by nlift_lref_be_SO/ #H #HV12 destruct
+lapply (H2X … HLK1 HLK2) -H2X /2 width=3 by nlift_lref_be_SO/
+/3 width=9 by or3_intro2, ex5_5_intro/
+qed-.
+
+lemma llpx_sn_alt_fwd_lref: ∀R,L1,L2,d,i. llpx_sn_alt R d (#i) L1 L2 →
+                            ∨∨ |L1| ≤ i ∧ |L2| ≤ i
+                             | yinj i < d
+                             | ∃∃I,K1,K2,V1,V2. ⇩[i] L1 ≡ K1.ⓑ{I}V1 &
+                                                ⇩[i] L2 ≡ K2.ⓑ{I}V2 &
+                                                llpx_sn_alt R (yinj 0) V1 K1 K2 &
+                                                R K1 V1 V2 & d ≤ yinj i.
+/2 width=3 by llpx_sn_alt_fwd_lref_aux/ qed-.
+
+(* Basic inversion lemmas ****************************************************)
+
+fact llpx_sn_alt_inv_flat_aux: ∀R,L1,L2,X,d. llpx_sn_alt R d X L1 L2 →
+                               ∀I,V,T. X = ⓕ{I}V.T →
+                               llpx_sn_alt R d V L1 L2 ∧ llpx_sn_alt R d T L1 L2.
+#R #L1 #L2 #X #d * -L1 -L2 -X -d
+#L1 #L2 #X #d #H1X #H2X #HL12
+#I #V #T #H destruct
+@conj @llpx_sn_alt_intro // -HL12
+/4 width=8 by nlift_flat_sn, nlift_flat_dx/
+qed-.
+
+lemma llpx_sn_alt_inv_flat: ∀R,I,L1,L2,V,T,d. llpx_sn_alt R d (ⓕ{I}V.T) L1 L2 →
+                            llpx_sn_alt R d V L1 L2 ∧ llpx_sn_alt R d T L1 L2.
+/2 width=4 by llpx_sn_alt_inv_flat_aux/ qed-.
+
+fact llpx_sn_alt_inv_bind_aux: ∀R,L1,L2,X,d. llpx_sn_alt R d X L1 L2 →
+                               ∀a,I,V,T. X = ⓑ{a,I}V.T →
+                               llpx_sn_alt R d V L1 L2 ∧ llpx_sn_alt R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V).
+#R #L1 #L2 #X #d * -L1 -L2 -X -d
+#L1 #L2 #X #d #H1X #H2X #HL12
+#a #I #V #T #H destruct
+@conj @llpx_sn_alt_intro [3,6: normalize /2 width=1 by eq_f2/ ] -HL12
+#I1 #I2 #K1 #K2 #W1 #W2 #i #Hdi #H #HLK1 #HLK2
+[1,2: /4 width=9 by nlift_bind_sn/ ]
+lapply (yle_inv_succ1 … Hdi) -Hdi * #Hdi #Hi
+lapply (ldrop_inv_drop1_lt … HLK1 ?) -HLK1 /2 width=1 by ylt_O/ #HLK1
+lapply (ldrop_inv_drop1_lt … HLK2 ?) -HLK2 /2 width=1 by ylt_O/ #HLK2
+[ @(H1X … HLK1 HLK2) | @(H2X … HLK1 HLK2) ] // -I1 -I2 -L1 -L2 -K1 -K2 -W1 -W2
+@nlift_bind_dx <plus_minus_m_m /2 width=2 by ylt_O/
+qed-.
+
+lemma llpx_sn_alt_inv_bind: ∀R,a,I,L1,L2,V,T,d. llpx_sn_alt R d (ⓑ{a,I}V.T) L1 L2 →
+                            llpx_sn_alt R d V L1 L2 ∧ llpx_sn_alt R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V).
+/2 width=4 by llpx_sn_alt_inv_bind_aux/ qed-.
+
+(* Basic properties **********************************************************)
+
+lemma llpx_sn_alt_intro_alt: ∀R,L1,L2,T,d. |L1| = |L2| →
+                             (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
+                                ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+                                ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn_alt R 0 V1 K1 K2
+                             ) → llpx_sn_alt R d T L1 L2.
+#R #L1 #L2 #T #d #HL12 #IH @llpx_sn_alt_intro // -HL12
+#I1 #I2 #K1 #K2 #HLK1 #HLK2 #i #Hid #HnT #HLK1 #HLK2
+elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /2 width=1 by conj/
+qed.
+
+lemma llpx_sn_alt_sort: ∀R,L1,L2,d,k. |L1| = |L2| → llpx_sn_alt R d (⋆k) L1 L2.
+#R #L1 #L2 #d #k #HL12 @llpx_sn_alt_intro // -HL12
+#I1 #I2 #K1 #K2 #V1 #V2 #i #_ #H elim (H (⋆k)) //
+qed.
+
+lemma llpx_sn_alt_gref: ∀R,L1,L2,d,p. |L1| = |L2| → llpx_sn_alt R d (§p) L1 L2.
+#R #L1 #L2 #d #p #HL12 @llpx_sn_alt_intro // -HL12
+#I1 #I2 #K1 #K2 #V1 #V2 #i #_ #H elim (H (§p)) //
+qed.
+
+lemma llpx_sn_alt_skip: ∀R,L1,L2,d,i. |L1| = |L2| → yinj i < d → llpx_sn_alt R d (#i) L1 L2.
+#R #L1 #L2 #d #i #HL12 #Hid @llpx_sn_alt_intro // -HL12
+#I1 #I2 #K1 #K2 #V1 #V2 #j #Hdj #H elim (H (#i)) -H
+/4 width=3 by lift_lref_lt, ylt_yle_trans, ylt_inv_inj/
+qed.
+
+lemma llpx_sn_alt_free: ∀R,L1,L2,d,i. |L1| ≤ i → |L2| ≤ i → |L1| = |L2| →
+                        llpx_sn_alt R d (#i) L1 L2.
+#R #L1 #L2 #d #i #HL1 #_ #HL12 @llpx_sn_alt_intro // -HL12
+#I1 #I2 #K1 #K2 #V1 #V2 #j #_ #H #HLK1 elim (H (#(i-1))) -H
+lapply (ldrop_fwd_length_lt2 … HLK1) -HLK1
+/3 width=3 by lift_lref_ge_minus, lt_to_le_to_lt/
+qed.
+
+lemma llpx_sn_alt_lref: ∀R,I,L1,L2,K1,K2,V1,V2,d,i. d ≤ yinj i →
+                        ⇩[i] L1 ≡ K1.ⓑ{I}V1 → ⇩[i] L2 ≡ K2.ⓑ{I}V2 →
+                        llpx_sn_alt R 0 V1 K1 K2 → R K1 V1 V2 →
+                        llpx_sn_alt R d (#i) L1 L2.
+#R #I #L1 #L2 #K1 #K2 #V1 #V2 #d #i #Hdi #HLK1 #HLK2 #HK12 #HV12 @llpx_sn_alt_intro
+[1,2: #Z1 #Z2 #Y1 #Y2 #X1 #X2 #j #Hdj #H #HLY1 #HLY2
+  elim (lt_or_eq_or_gt i j) #Hij destruct
+  [1,4: elim (H (#i)) -H /2 width=1 by lift_lref_lt/
+  |2,5: lapply (ldrop_mono … HLY1 … HLK1) -HLY1 -HLK1 #H destruct
+    lapply (ldrop_mono … HLY2 … HLK2) -HLY2 -HLK2 #H destruct /2 width=1 by conj/
+  |3,6: elim (H (#(i-1))) -H /2 width=1 by lift_lref_ge_minus/
+  ]
+| lapply (llpx_sn_alt_fwd_length … HK12) -HK12 #HK12
+  @(ldrop_fwd_length_eq2 … HLK1 HLK2) normalize /2 width=1 by eq_f2/
+]
+qed.
+
+fact llpx_sn_alt_flat_aux: ∀R,I,L1,L2,V,d. llpx_sn_alt R d V L1 L2 →
+                           ∀Y1,Y2,T,m. llpx_sn_alt R m T Y1 Y2 →
+                           Y1 = L1 → Y2 = L2 → m = d →
+                           llpx_sn_alt R d (ⓕ{I}V.T) L1 L2.
+#R #I #L1 #L2 #V #d * -L1 -L2 -V -d #L1 #L2 #V #d #H1V #H2V #HL12
+#Y1 #Y2 #T #m * -Y1 -Y2 -T -m #Y1 #Y2 #T #m #H1T #H2T #_
+#HT1 #HY2 #Hm destruct
+@llpx_sn_alt_intro // -HL12
+#J1 #J2 #K1 #K2 #W1 #W2 #i #Hdi #HnVT #HLK1 #HLK2
+elim (nlift_inv_flat … HnVT) -HnVT /3 width=8 by/
+qed-.
+
+lemma llpx_sn_alt_flat: ∀R,I,L1,L2,V,T,d.
+                        llpx_sn_alt R d V L1 L2 → llpx_sn_alt R d T L1 L2 →
+                        llpx_sn_alt R d (ⓕ{I}V.T) L1 L2.
+/2 width=7 by llpx_sn_alt_flat_aux/ qed.
+
+fact llpx_sn_alt_bind_aux: ∀R,a,I,L1,L2,V,d. llpx_sn_alt R d V L1 L2 →
+                           ∀Y1,Y2,T,m. llpx_sn_alt R m T Y1 Y2 →
+                           Y1 = L1.ⓑ{I}V → Y2 = L2.ⓑ{I}V → m = ⫯d →
+                           llpx_sn_alt R d (ⓑ{a,I}V.T) L1 L2.
+#R #a #I #L1 #L2 #V #d * -L1 -L2 -V -d #L1 #L2 #V #d #H1V #H2V #HL12
+#Y1 #Y2 #T #m * -Y1 -Y2 -T -m #Y1 #Y2 #T #m #H1T #H2T #_
+#HT1 #HY2 #Hm destruct
+@llpx_sn_alt_intro // -HL12
+#J1 #J2 #K1 #K2 #W1 #W2 #i #Hdi #HnVT #HLK1 #HLK2
+elim (nlift_inv_bind … HnVT) -HnVT /3 width=8 by ldrop_drop, yle_succ/
+qed-.
+
+lemma llpx_sn_alt_bind: ∀R,a,I,L1,L2,V,T,d.
+                        llpx_sn_alt R d V L1 L2 →
+                        llpx_sn_alt R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) →
+                        llpx_sn_alt R d (ⓑ{a,I}V.T) L1 L2.
+/2 width=7 by llpx_sn_alt_bind_aux/ qed.
+
+(* Main properties **********************************************************)
+
+theorem llpx_sn_lpx_sn_alt: ∀R,L1,L2,T,d. llpx_sn R d T L1 L2 → llpx_sn_alt R d T L1 L2.
+#R #L1 #L2 #T #d #H elim H -L1 -L2 -T -d
+/2 width=9 by llpx_sn_alt_sort, llpx_sn_alt_gref, llpx_sn_alt_skip, llpx_sn_alt_free, llpx_sn_alt_lref, llpx_sn_alt_flat, llpx_sn_alt_bind/
+qed.
+
+(* Main inversion lemmas ****************************************************)
+
+theorem llpx_sn_alt_inv_lpx_sn: ∀R,T,L1,L2,d. llpx_sn_alt R d T L1 L2 → llpx_sn R d T L1 L2.
+#R #T #L1 @(f2_ind … rfw … L1 T) -L1 -T #n #IH #L1 * *
+[1,3: /3 width=4 by llpx_sn_alt_fwd_length, llpx_sn_gref, llpx_sn_sort/
+| #i #Hn #L2 #d #H lapply (llpx_sn_alt_fwd_length … H)
+  #HL12 elim (llpx_sn_alt_fwd_lref … H) -H
+  [ * /2 width=1 by llpx_sn_free/
+  | /2 width=1 by llpx_sn_skip/
+  | * /4 width=9 by llpx_sn_lref, ldrop_fwd_rfw/
+  ]
+| #a #I #V #T #Hn #L2 #d #H elim (llpx_sn_alt_inv_bind … H) -H
+  /3 width=1 by llpx_sn_bind/
+| #I #V #T #Hn #L2 #d #H elim (llpx_sn_alt_inv_flat … H) -H
+  /3 width=1 by llpx_sn_flat/
+]
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma llpx_sn_intro_alt: ∀R,L1,L2,T,d. |L1| = |L2| →
+                         (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
+                            ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+                            ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn R 0 V1 K1 K2
+                         ) → llpx_sn R d T L1 L2.
+#R #L1 #L2 #T #d #HL12 #IH @llpx_sn_alt_inv_lpx_sn
+@llpx_sn_alt_intro_alt // -HL12
+#I1 #I2 #K1 #K2 #HLK1 #HLK2 #i #Hid #HnT #HLK1 #HLK2
+elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /3 width=1 by llpx_sn_lpx_sn_alt, and3_intro/
+qed.
+
+(* Advanced forward lemmas lemmas *******************************************)
+
+lemma llpx_sn_fwd_alt: ∀R,L1,L2,T,d. llpx_sn R d T L1 L2 →
+                       |L1| = |L2| ∧
+                       ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
+                       ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+                       ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn R 0 V1 K1 K2.
+#R #L1 #L2 #T #d #H lapply (llpx_sn_lpx_sn_alt … H) -H
+#H elim (llpx_sn_alt_fwd_gen … H) -H
+#HL12 #IH @conj //
+#I1 #I2 #K1 #K2 #HLK1 #HLK2 #i #Hid #HnT #HLK1 #HLK2
+elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /3 width=1 by llpx_sn_alt_inv_lpx_sn, and3_intro/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/lpx_conj.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/lpx_conj.etc
new file mode 100644
index 000000000..5950f1b92
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/lpx_conj.etc
@@ -0,0 +1,120 @@
+include "basic_2/relocation/lleq_alt.ma".
+include "basic_2/reduction/cpx_lleq.ma".
+include "basic_2/reduction/lpx_lleq.ma".
+
+lemma not_ex_to_all_not: ∀A:Type[0]. ∀R:predicate A.
+                         ((∃a. R a)→⊥) → (∀a. R a → ⊥).
+/3 width=2 by ex_intro/ qed-.
+
+lemma lt_repl_sn_trans_tw: ∀L1,L2,T1,T2. ♯{L1, T1} < ♯{L2, T2} →
+                           ∀U1. ♯{U1} = ♯{T1} → ♯{L1, U1} < ♯{L2, T2}.
+normalize in ⊢ (?→?→?→?→?%%→?→?→?%%); //
+qed-.
+
+axiom cpx_fwd_lift1: ∀h,g,G,L,U1,U2. ⦃G, L⦄ ⊢ U1 ➡[h, g] U2 →
+                     ∀T1,d,e. ⇧[d, e] T1 ≡ U1 → ∃T2. ⇧[d, e] T2 ≡ U2.
+(*
+#h #g #G #L #U1 #U2 #H elim H -G -L -U1 -U2
+[ * #i #G #L #T1 #d #e #H
+  [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=2 by ex_intro/
+  | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=2 by lift_lref_ge_minus, lift_lref_lt, ex_intro/
+  | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=2 by ex_intro/
+  ]
+| #G #L #k #l #Hkl #T1 #d #e #H
+  lapply (lift_inv_sort2 … H) -H #H destruct /3 width=3 by ex_intro/
+| #I #G #L #K #V1 #V2 #W2 #i #HLK #HV12 #HVW2 #IHV2 #T1 #d #e #H
+  elim (lift_inv_lref2 … H) -H * #Hid #H destruct
+  [ elim (ldrop_conf_lt … HLK … HLV) -L // #L #U #HKL #HLV #HUV
+    elim (IHV2 … HLV … HUV) -V #U2 #HUV2 #HU2
+    elim (lift_trans_le … HUV2 … HVW2) -V2 // >minus_plus <plus_minus_m_m /3 width=9 by cpx_delta, ex2_intro/
+  | elim (le_inv_plus_l … Hid) #Hdie #Hei
+    lapply (ldrop_conf_ge … HLK … HLV ?) -L // #HKLV
+    elim (lift_split … HVW2 d (i - e + 1)) -HVW2 /3 width=1 by le_S, le_S_S/ -Hid -Hdie
+    #V1 #HV1 >plus_minus // <minus_minus /2 width=1 by le_S/ <minus_n_n <plus_n_O /3 width=9 by cpx_delta, ex2_intro/
+  ]
+| #a #I #G #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #s #d #e #HLK #X #H
+  elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
+  elim (IHV12 … HLK … HWV1) -IHV12 #W2 #HW12 #HWV2
+  elim (IHU12 … HTU1) -IHU12 -HTU1 /3 width=6 by cpx_bind, ldrop_skip, lift_bind, ex2_intro/
+| #I #G #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #s #d #e #HLK #X #H
+  elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
+  elim (IHV12 … HLK … HWV1) -V1
+  elim (IHU12 … HLK … HTU1) -U1 -HLK /3 width=5 by cpx_flat, lift_flat, ex2_intro/
+| #G #L #V #U1 #U #U2 #_ #HU2 #IHU1 #K #s #d #e #HLK #X #H
+  elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
+  elim (IHU1 (K.ⓓW1) s … HTU1) /2 width=1/ -L -U1 #T #HTU #HT1
+  elim (lift_div_le … HU2 … HTU) -U /3 width=5 by cpx_zeta, ex2_intro/
+| #G #L #V #U1 #U2 #_ #IHU12 #K #s #d #e #HLK #X #H
+  elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
+  elim (IHU12 … HLK … HTU1) -L -U1 /3 width=3 by cpx_tau, ex2_intro/
+| #G #L #V1 #V2 #U1 #_ #IHV12 #K #s #d #e #HLK #X #H
+  elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
+  elim (IHV12 … HLK … HWV1) -L -V1 /3 width=3 by cpx_ti, ex2_intro/
+| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #K #s #d #e #HLK #X #HX
+  elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct
+  elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct
+  elim (IHV12 … HLK … HV01) -V1 #V3 #HV32 #HV03
+  elim (IHT12 (K.ⓛW0) s … HT01) -T1 /2 width=1 by ldrop_skip/ #T3 #HT32 #HT03
+  elim (IHW12 … HLK … HW01) -W1
+  /4 width=7 by cpx_beta, lift_bind, lift_flat, ex2_intro/
+| #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #K #s #d #e #HLK #X #HX
+  elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct
+  elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct
+  elim (IHV1 … HLK … HV01) -V1 #V3 #HV3 #HV03
+  elim (IHT12 (K.ⓓW0) s … HT01) -T1 /2 width=1 by ldrop_skip/ #T3 #HT32 #HT03
+  elim (IHW12 … HLK … HW01) -W1 #W3 #HW32 #HW03
+  elim (lift_trans_le … HV3 … HV2) -V
+  /4 width=9 by cpx_theta, lift_bind, lift_flat, ex2_intro/
+]
+qed-.
+*)
+lemma cpx_fwd_nlift2: ∀h,g,G,L,U1,U2. ⦃G, L⦄ ⊢ U1 ➡[h, g] U2 → ∀d,e.
+                      (∀T2. ⇧[d, e] T2 ≡ U2 → ⊥) → (∀T1. ⇧[d, e] T1 ≡ U1 → ⊥).
+#h #g #G #L #U1 #U2 #HU12 #d #e #HnU2 #T1 #HTU1
+elim (cpx_fwd_lift1 … HU12 … HTU1) -L -U1 /2 width=2 by/
+qed-.
+
+fact lleq_lpx_cpx_trans_aux: ∀h,g,G,T1,L1s,L1d,d. L1s ⋕[T1, d] L1d →
+                             ∀Y,L2d. ⦃G, Y⦄ ⊢ ➡[h, g] L2d → Y = L1d → d = 0 →
+                             ∀T2. ⦃G, L1d⦄ ⊢ T1 ➡[h, g] T2 →
+                             ∃∃L2s. ⦃G, L1s⦄ ⊢ ➡[h, g] L2s & L2s ⋕[T2, d] L2d.
+#h #g #G #T1 #L1s @(f2_ind … rfw … L1s T1) -L1s -T1 #n #IH
+#Ys #U1 #Hn #Yd #d #HU1 elim (lleq_fwd_alt … HU1) #H #IHU1
+#Y #L2d * -Y -L2d
+[ -IH -IHU1 -HU1 #HY #Hd #U2 #HU12 destruct
+  >(length_inv_zero_dx … H) -Ys /2 width=3 by ex2_intro/
+| #Id #L1d #L2d #W1d #W2d #HL12d #HW12d #HY #Hd #U2 #HU12 destruct
+  elim (length_inv_pos_dx … H) -H #Is #L1s #W1s #_ #H destruct
+  elim (is_lift_dec U1 0 1) [ -IHU1 -HW12d | -HU1 ]
+  [ * #T1 #HTU1 lapply (lift_fwd_tw … HTU1) #H
+    lapply (lleq_inv_lift_le … HU1 L1s L1d … HTU1 ?) -HU1 /2 width=1 by ldrop_drop/
+    #HT1 elim (cpx_inv_lift1 … HU12 L1d … HTU1) -HU12 -HTU1 /2 width=4 by ldrop_drop/
+    #T2 #HTU2 #HT12 elim (IH … HT1 … HL12d … HT12) /2 width=3 by lt_repl_sn_trans_tw/ -IH -HT1 -HT12 -H
+    #L2s #HL12s #HT2 @(ex2_intro … (L2s.ⓑ{Is}W1s))
+    /3 width=10 by lleq_lift_le, lpx_pair, ldrop_drop/ (**) (* full auto too slow *)
+  | #HnU1 lapply (not_ex_to_all_not … HnU1) -HnU1 #HnU1
+    elim (IHU1 … HnU1) [2,3,4: // |5,6,7,8,9,10: skip ] -HnU1 #H1 #H2 #HW1s destruct
+    elim (IH … HW1s … HL12d … HW12d) // #L2s #HL12s #HW2d
+    @(ex2_intro … (L2s.ⓑ{Id}W2d)) /3 width=3 by lleq_cpx_trans, lpx_pair/
+    lapply (lleq_fwd_length … HW2d) #HL2sd -HW12d -HW1s
+    @lleq_intro_alt [ normalize // ] -HL2sd
+    #I2s #I2d #K2s #K2d #V2s #V2d #i @(nat_ind_plus … i) -i
+    [ #_ #_ #HLK2s #HLK2d -IH -IHU1 -HU12 -HL12s -HL12d
+      lapply (ldrop_inv_O2 … HLK2s) -HLK2s #H destruct
+      lapply (ldrop_inv_O2 … HLK2d) -HLK2d #H destruct /2 width=1 by and3_intro/
+    | #i #_ #_ #HnU2 #HLK2s #HLK2d
+      lapply (cpx_fwd_nlift2 … HU12 … HnU2) -HU12 -HnU2 #HnU1
+      lapply (ldrop_inv_drop1 … HLK2s) -HLK2s #HLK2s
+      lapply (ldrop_inv_drop1 … HLK2d) -HLK2d #HLK2d
+      elim (lpx_ldrop_trans_O1 … HL12s … HLK2s) -L2s #Y #HLK1s #H
+      elim (lpx_inv_pair2 … H) -H #K1s #V1s #HK12s #HV12s #H destruct
+      elim (lpx_ldrop_trans_O1 … HL12d … HLK2d) -L2d #Y #HLK1d #H
+      elim (lpx_inv_pair2 … H) -H #K1d #V1d #HK12d #HV12d #H destruct
+      elim (IHU1 … HnU1) [2,3,4: /2 width=2 by ldrop_drop/ | 5,6,7,8,9,10: skip ] -IHU1 -HnU1 -HLK1d
+      #H1 #H2 #HV1d destruct
+      lapply (ldrop_fwd_rfw … HLK1s) -HLK1s #H
+      elim (IH … HV1d … HK12d … HV12d) // -IH -HV1d -HK12d -HV12d
+      [ #Y #H1Y #H2Y   
+       
+      
+
diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_restricted_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_restricted_weight.ma
index e889b0548..3669ca151 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_restricted_weight.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_restricted_weight.ma
@@ -40,6 +40,10 @@ lemma rfw_lpair_sn: ∀I,L,V,T. ♯{L, V} < ♯{L.ⓑ{I}V, T}.
 normalize /3 width=1 by monotonic_lt_plus_l, monotonic_le_plus_r/
 qed.
 
+lemma rfw_lpair_dx: ∀I,L,V,T. ♯{L, T} < ♯{L.ⓑ{I}V, T}.
+normalize /3 width=1 by monotonic_lt_plus_l, monotonic_le_plus_r/
+qed.
+
 (* Basic_1: removed theorems 7:
             flt_thead_sx flt_thead_dx flt_trans
             flt_arith0 flt_arith1 flt_arith2 flt_wf_ind
diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma
index aa20d64db..d7c923dd4 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma
@@ -39,7 +39,7 @@ normalize in ⊢ (?→?→?→?→?→?%%); //
 qed.
 
 lemma fw_lpair_sn: ∀I,G,L,V,T. ♯{G, L, V} < ♯{G, L.ⓑ{I}V, T}.
-normalize /3 width=1 by monotonic_lt_plus_l, monotonic_le_plus_r/ (**) (* auto too slow without trace *)
+normalize /3 width=1 by monotonic_lt_plus_l, monotonic_le_plus_r/
 qed.
 
 (* Basic_1: removed theorems 7:
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazypredsn_7.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazypredsn_7.ma
new file mode 100644
index 000000000..2350f5efc
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazypredsn_7.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G , break term 46 L1 ⦄ ⊢ ➡ break [ term 46 h , break term 46 g , break term 46 T , break term 46 d ] break term 46 L2 )"
+   non associative with precedence 45
+   for @{ 'LazyPRedSn $G $L1 $L2 $h $g $T $d }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_lift.ma
index dcd6307a7..101e2b029 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_lift.ma
@@ -61,7 +61,7 @@ qed.
 (* Basic_1: includes: pr0_gen_lift pr2_gen_lift *)
 lemma cpr_inv_lift1: ∀G. l_deliftable_sn (cpr G).
 #G #L #U1 #U2 #H elim H -G -L -U1 -U2
-[ * #G #L #i #K #s #d #e #_ #T1 #H
+[ * #i #G #L #K #s #d #e #_ #T1 #H
   [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by ex2_intro/
   | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by lift_lref_ge_minus, lift_lref_lt, ex2_intro/
   | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by ex2_intro/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
index d43413c97..45e71b66e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
@@ -84,7 +84,7 @@ qed.
 
 lemma cpx_inv_lift1: ∀h,g,G. l_deliftable_sn (cpx h g G).
 #h #g #G #L #U1 #U2 #H elim H -G -L -U1 -U2
-[ * #G #L #i #K #s #d #e #_ #T1 #H
+[ * #i #G #L #K #s #d #e #_ #T1 #H
   [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by cpx_atom, lift_sort, ex2_intro/
   | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by cpx_atom, lift_lref_ge_minus, lift_lref_lt, ex2_intro/
   | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by cpx_atom, lift_gref, ex2_intro/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma
index ae6ddac78..d2703ad7c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma
@@ -12,9 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/relocation/lleq_leq.ma".
 include "basic_2/relocation/lleq_ldrop.ma".
-include "basic_2/reduction/cpx.ma".
+include "basic_2/reduction/cpx_llpx_sn.ma".
 
 (* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************)
 
@@ -44,36 +43,10 @@ lemma lleq_cpx_trans: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 →
 ]
 qed-.
 
-(* Note: lemma 1000 *)
-lemma lleq_cpx_conf_dx: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 →
-                        ∀L1. L1 ⋕[T1, 0] L2 → L1 ⋕[T2, 0] L2.
-#h #g #G #L2 #T1 #T2 #H elim H -G -L2 -T1 -T2
-[ //
-| /3 width=3 by lleq_fwd_length, lleq_sort/
-| #I #G #L2 #K2 #V1 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV12 #L1 #H elim (lleq_inv_lref_ge_dx … H … HLK2) // -H
-  #K1 #HLK1 #HV1
-  lapply (ldrop_fwd_drop2 … HLK1) -HLK1 #HLK1
-  lapply (ldrop_fwd_drop2 … HLK2) -HLK2 #HLK2
-  @(lleq_lift_le … HLK1 HLK2 … HVW2) -HLK1 -HLK2 -HVW2 /2 width=1 by/ (**) (* full auto too slow *)
-| #a #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #H elim (lleq_inv_bind_O … H) -H
-  /4 width=5 by lleq_bind_repl_SO, lleq_bind/
-| #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #H elim (lleq_inv_flat … H) -H
-  /3 width=1 by lleq_flat/
-| #G #L2 #V #T1 #T2 #T #_ #HT2 #IHT12 #L1 #H elim (lleq_inv_bind_O … H) -H
-  /3 width=10 by lleq_inv_lift_le, ldrop_drop/
-| #G #L2 #V #T1 #T2 #_ #IHT12 #L1 #H elim (lleq_inv_flat … H) -H /2 width=1 by/
-| #G #L2 #V1 #V2 #T #_ #IHV12 #L1 #H elim (lleq_inv_flat … H) -H /2 width=1 by/
-| #a #G #L2 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L1 #H elim (lleq_inv_flat … H) -H
-  #HV1 #H elim (lleq_inv_bind_O … H) -H
-  /4 width=5 by lleq_bind_repl_SO, lleq_flat, lleq_bind/
-| #a #G #L2 #V1 #V2 #V #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #L1 #H elim (lleq_inv_flat … H) -H
-  #HV1 #H elim (lleq_inv_bind_O … H) -H
-  #HW1 #HT1 @lleq_bind_O /2 width=1 by/ @lleq_flat (**) (* full auto too slow *)
-  [ /3 width=10 by lleq_lift_le, ldrop_drop/
-  | /3 width=3 by lleq_bind_repl_O/
-]
-qed-.
-
 lemma lleq_cpx_conf_sn: ∀h,g,G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2 →
                         ∀L2. L1 ⋕[T1, 0] L2 → L1 ⋕[T2, 0] L2.
-/4 width=6 by lleq_cpx_conf_dx, lleq_sym/ qed-.
+/3 width=6 by llpx_sn_cpx_conf, lift_mono, ex2_intro/ qed-.
+
+lemma lleq_cpx_conf_dx: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 →
+                        ∀L1. L1 ⋕[T1, 0] L2 → L1 ⋕[T2, 0] L2.
+/4 width=6 by lleq_cpx_conf_sn, lleq_sym/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_llpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_llpx_sn.ma
new file mode 100644
index 000000000..38a83a760
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_llpx_sn.ma
@@ -0,0 +1,51 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/relocation/llpx_sn_ldrop.ma".
+include "basic_2/reduction/cpx.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************)
+
+(* Properties on lazy sn pointwise extensions *******************************)
+
+(* Note: lemma 1000 *)
+lemma llpx_sn_cpx_conf: ∀R. (∀L. reflexive … (R L)) → l_liftable R → l_deliftable_sn R →
+                        ∀h,g,G,Ls,T1,T2. ⦃G, Ls⦄ ⊢ T1 ➡[h, g] T2 →
+                        ∀Ld. llpx_sn R 0 T1 Ls Ld → llpx_sn R 0 T2 Ls Ld.
+#R #H1R #H2R #H3R #h #g #G #Ls #T1 #T2 #H elim H -G -Ls -T1 -T2
+[ //
+| /3 width=4 by llpx_sn_fwd_length, llpx_sn_sort/
+| #I #G #Ls #Ks #V1s #V2s #W2s #i #HLKs #_ #HVW2s #IHV12s #Ld #H elim (llpx_sn_inv_lref_ge_sn … H … HLKs) // -H
+  #Kd #V1d #HLKd #HV1s #HV1sd
+  lapply (ldrop_fwd_drop2 … HLKs) -HLKs #HLKs
+  lapply (ldrop_fwd_drop2 … HLKd) -HLKd #HLKd
+  @(llpx_sn_lift_le … HLKs HLKd … HVW2s) -HLKs -HLKd -HVW2s /2 width=1 by/ (**) (* full auto too slow *)
+| #a #I #G #Ls #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #Ld #H elim (llpx_sn_inv_bind_O … H) -H
+  /4 width=5 by llpx_sn_bind_repl_SO, llpx_sn_bind/
+| #I #G #Ls #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H
+  /3 width=1 by llpx_sn_flat/
+| #G #Ls #V #T1 #T2 #T #_ #HT2 #IHT12 #Ld #H elim (llpx_sn_inv_bind_O … H) -H
+  /3 width=10 by llpx_sn_inv_lift_le, ldrop_drop/
+| #G #Ls #V #T1 #T2 #_ #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H /2 width=1 by/
+| #G #Ls #V1 #V2 #T #_ #IHV12 #Ld #H elim (llpx_sn_inv_flat … H) -H /2 width=1 by/
+| #a #G #Ls #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H
+  #HV1 #H elim (llpx_sn_inv_bind_O … H) -H
+  /4 width=5 by llpx_sn_bind_repl_SO, llpx_sn_flat, llpx_sn_bind/
+| #a #G #Ls #V1 #V2 #V #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H
+  #HV1 #H elim (llpx_sn_inv_bind_O … H) -H //
+  #HW1 #HT1 @llpx_sn_bind_O /2 width=1 by/ @llpx_sn_flat (**) (* full auto too slow *)
+  [ /3 width=10 by llpx_sn_lift_le, ldrop_drop/
+  | /3 width=4 by llpx_sn_bind_repl_O/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpr_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpr_ldrop.ma
index 453f21ddc..a19534b4a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpr_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpr_ldrop.ma
@@ -46,20 +46,7 @@ lemma llpr_inv_bind_O: ∀a,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ➡ [ⓑ{a,I}V.T, 0]
 lemma llpr_bind_repl_O: ∀I,G,L1,L2,V1,V2,T. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡[T, 0] L2.ⓑ{I}V2 →
                         ∀J,W1,W2. ⦃G, L1⦄ ⊢ ➡[W1, 0] L2 → ⦃G, L1⦄ ⊢ W1 ➡ W2 → ⦃G, L1.ⓑ{J}W1⦄ ⊢ ➡[T, 0] L2.ⓑ{J}W2.
 /2 width=4 by llpx_sn_bind_repl_O/ qed-.
-(*
-(* Properies on local environment slicing ***********************************)
 
-(* Basic_1: includes: wcpr0_drop *)
-lemma lpr_ldrop_conf: ∀G. dropable_sn (lpr G).
-/3 width=6 by lpx_sn_deliftable_dropable, cpr_inv_lift1/ qed-.
-
-(* Basic_1: includes: wcpr0_drop_back *)
-lemma ldrop_lpr_trans: ∀G. dedropable_sn (lpr G).
-/3 width=10 by lpx_sn_liftable_dedropable, cpr_lift/ qed-.
-
-lemma lpr_ldrop_trans_O1: ∀G. dropable_dx (lpr G).
-/2 width=3 by lpx_sn_dropable/ qed-.
-*)
 (* Properties on context-sensitive parallel reduction for terms *************)
 
 lemma fqu_cpr_trans_dx: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx.ma
new file mode 100644
index 000000000..ef71c6515
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx.ma
@@ -0,0 +1,57 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/notation/relations/lazypredsn_7.ma".
+include "basic_2/reduction/llpr.ma".
+include "basic_2/reduction/cpx.ma".
+
+(* LAZY SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ***************)
+
+definition llpx: ∀h. sd h → genv → relation4 ynat term lenv lenv ≝
+                 λh,g,G. llpx_sn (cpx h g  G).
+
+interpretation "lazy extended parallel reduction (local environment, sn variant)"
+   'LazyPRedSn G L1 L2 h g T d = (llpx h g G d T L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma llpx_inv_flat: ∀h,g,I,G,L1,L2,V,T,d. ⦃G, L1⦄ ⊢ ➡[h, g, ⓕ{I}V.T, d] L2 →
+                     ⦃G, L1⦄ ⊢ ➡[h, g, V, d] L2 ∧ ⦃G, L1⦄ ⊢ ➡[h, g, T, d] L2.
+/2 width=2 by llpx_sn_inv_flat/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma llpx_fwd_length: ∀h,g,G,L1,L2,T,d. ⦃G, L1⦄ ⊢ ➡[h, g, T, d] L2 → |L1| = |L2|.
+/2 width=4 by llpx_sn_fwd_length/ qed-.
+
+lemma llpx_fwd_flat_dx: ∀h,g,I,G,L1,L2,V,T,d. ⦃G, L1⦄ ⊢ ➡[h, g, ⓕ{I}V.T, d] L2 →
+                     ⦃G, L1⦄ ⊢ ➡[h, g, T, d] L2.
+/2 width=3 by llpx_sn_fwd_flat_dx/ qed-.
+
+lemma llpx_fwd_pair_sn: ∀h,g,I,G,L1,L2,V,T,d. ⦃G, L1⦄ ⊢ ➡[h, g, ②{I}V.T, d] L2 →
+                        ⦃G, L1⦄ ⊢ ➡[h, g, V, d] L2.
+/2 width=3 by llpx_sn_fwd_pair_sn/ qed-.
+
+(* Basic properties *********************************************************)
+
+lemma llpx_lref: ∀h,g,I,G,L1,L2,K1,K2,V1,V2,d,i. d ≤ yinj i →
+                 ⇩[i] L1 ≡ K1.ⓑ{I}V1 → ⇩[i] L2 ≡ K2.ⓑ{I}V2 →
+                 ⦃G, K1⦄ ⊢ ➡[h, g, V1, 0] K2 → ⦃G, K1⦄ ⊢ V1 ➡[h, g] V2 → ⦃G, L1⦄ ⊢ ➡[h, g, #i, d] L2.
+/2 width=9 by llpx_sn_lref/ qed.
+
+lemma llpx_refl: ∀h,g,G,T,d. reflexive … (llpx h g G d T).
+/2 width=1 by llpx_sn_refl/ qed.
+
+lemma llpr_llpx: ∀h,g,G,L1,L2,T,d. ⦃G, L1⦄ ⊢ ➡[T, d] L2 → ⦃G, L1⦄ ⊢ ➡[h, g, T, d] L2.
+/3 width=3 by llpx_sn_co, cpr_cpx/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_ldrop.ma
new file mode 100644
index 000000000..9b7d295d3
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_ldrop.ma
@@ -0,0 +1,91 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/reduction/cpx_llpx_sn.ma".
+include "basic_2/reduction/cpx_lift.ma".
+include "basic_2/reduction/llpx.ma".
+
+(* LAZY SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ***************)
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma llpx_inv_lref_ge_dx: ∀h,g,G,L1,L2,d,i. ⦃G, L1⦄ ⊢ ➡[h, g, #i, d] L2 → d ≤ i →
+                           ∀I,K2,V2. ⇩[i] L2 ≡ K2.ⓑ{I}V2 →
+                           ∃∃K1,V1. ⇩[i] L1 ≡ K1.ⓑ{I}V1 &
+                                    ⦃G, K1⦄ ⊢ ➡[h, g, V1, 0] K2 & ⦃G, K1⦄ ⊢ V1 ➡[h, g] V2.
+/2 width=5 by llpx_sn_inv_lref_ge_dx/ qed-.
+
+lemma llpx_inv_lref_ge_sn: ∀h,g,G,L1,L2,d,i. ⦃G, L1⦄ ⊢ ➡[h, g, #i, d] L2 → d ≤ i →
+                           ∀I,K1,V1. ⇩[i] L1 ≡ K1.ⓑ{I}V1 →
+                           ∃∃K2,V2. ⇩[i] L2 ≡ K2.ⓑ{I}V2 &
+                                    ⦃G, K1⦄ ⊢ ➡[h, g, V1, 0] K2 & ⦃G, K1⦄ ⊢ V1 ➡[h, g] V2.
+/2 width=5 by llpx_sn_inv_lref_ge_sn/ qed-.
+
+lemma llpx_inv_lref_ge_bi: ∀h,g,G,L1,L2,d,i. ⦃G, L1⦄ ⊢ ➡[h, g, #i, d] L2 → d ≤ i →
+                           ∀I1,I2,K1,K2,V1,V2.
+                           ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+                           ∧∧ I1 = I2 & ⦃G, K1⦄ ⊢ ➡[h, g, V1, 0] K2 & ⦃G, K1⦄ ⊢ V1 ➡[h, g] V2.
+/2 width=8 by llpx_sn_inv_lref_ge_bi/ qed-.
+
+lemma llpx_inv_bind_O: ∀h,g,a,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ➡ [h, g, ⓑ{a,I}V.T, 0] L2 →
+                       ⦃G, L1⦄ ⊢ ➡[h, g, V, 0] L2 ∧ ⦃G, L1.ⓑ{I}V⦄ ⊢ ➡[h, g, T, 0] L2.ⓑ{I}V.
+/2 width=2 by llpx_sn_inv_bind_O/ qed-.
+
+lemma llpx_bind_repl_O: ∀h,g,I,G,L1,L2,V1,V2,T. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡[h, g, T, 0] L2.ⓑ{I}V2 →
+                        ∀J,W1,W2. ⦃G, L1⦄ ⊢ ➡[h, g, W1, 0] L2 → ⦃G, L1⦄ ⊢ W1 ➡[h, g] W2 → ⦃G, L1.ⓑ{J}W1⦄ ⊢ ➡[h, g, T, 0] L2.ⓑ{J}W2.
+/2 width=4 by llpx_sn_bind_repl_O/ qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma llpx_fwd_bind_O_dx: ∀h,g,a,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ➡[h, g, ⓑ{a,I}V.T, 0] L2 →
+                          ⦃G, L1.ⓑ{I}V⦄ ⊢ ➡[h, g, T, 0] L2.ⓑ{I}V.
+/2 width=3 by llpx_sn_fwd_bind_O_dx/ qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma llpx_cpx_conf: ∀h,g,G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2 →
+                     ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g, T1, 0] L2 → ⦃G, L1⦄ ⊢ ➡[h, g, T2, 0] L2.
+/3 width=10 by llpx_sn_cpx_conf, cpx_inv_lift1, cpx_lift/ qed-.
+
+(* Inversion lemmas on relocation *******************************************)
+
+lemma llpx_ldrop_trans_O: ∀h,g,G,L1,L2,U. ⦃G, L1⦄ ⊢ ➡[h, g, U, 0] L2 →
+                          ∀K2,e. ⇩[e] L2 ≡ K2 → ∀T. ⇧[0, e] T ≡ U →
+                          ∃∃K1. ⇩[e] L1 ≡ K1 & ⦃G, K1⦄ ⊢ ➡[h, g, T, 0] K2.
+/2 width=5 by llpx_sn_ldrop_trans_O/ qed-.
+
+(* Properties on supclosure *************************************************)
+
+lemma llpx_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
+                      ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g, T1, 0] L1 →
+                      ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g, T2, 0] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+/3 width=7 by llpx_fwd_bind_O_dx, llpx_fwd_pair_sn,llpx_fwd_flat_dx, ex3_2_intro/
+[ #I #G1 #L1 #V1 #K1 #H elim (llpx_inv_lref_ge_dx … H) -H [5,6: // |2,3,4: skip ]
+  #Y1 #W1 #HKL1 #HW1 #HWV1 elim (lift_total V1 0 1)
+  /4 width=7 by llpx_cpx_conf, cpx_delta, fqu_drop, ldrop_fwd_drop2, ex3_2_intro/
+| #G #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #L0 #HU1
+  elim (llpx_ldrop_trans_O … HU1 … HLK1) -L1
+  /3 width=5 by fqu_drop, ex3_2_intro/
+]
+qed-.
+
+lemma llpx_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+                       ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g, T1, 0] L1 →
+                       ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g, T2, 0] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #HKL1 elim (fquq_inv_gen … H) -H
+[ #HT12 elim (llpx_fqu_trans … HT12 … HKL1) /3 width=5 by fqu_fquq, ex3_2_intro/
+| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lift_neg.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lift_neg.ma
deleted file mode 100644
index 220748ed3..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lift_neg.ma
+++ /dev/null
@@ -1,60 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/relocation/lift.ma".
-
-(* BASIC TERM RELOCATION ****************************************************)
-
-(* Properties on negated basic relocation ***********************************)
-
-lemma nlift_lref_be_SO: ∀X,i. ⇧[i, 1] X ≡ #i → ⊥.
-/2 width=7 by lift_inv_lref2_be/ qed-.
-
-lemma nlift_bind_sn: ∀W,d,e. (∀V. ⇧[d, e] V ≡ W → ⊥) →
-                     ∀a,I,U. (∀X. ⇧[d, e] X ≡ ⓑ{a,I}W.U → ⊥).
-#W #d #e #HW #a #I #U #X #H elim (lift_inv_bind2 … H) -H /2 width=2 by/
-qed-.
-
-lemma nlift_bind_dx: ∀U,d,e. (∀T. ⇧[d+1, e] T ≡ U → ⊥) →
-                     ∀a,I,W. (∀X. ⇧[d, e] X ≡ ⓑ{a,I}W.U → ⊥).
-#U #d #e #HU #a #I #W #X #H elim (lift_inv_bind2 … H) -H /2 width=2 by/
-qed-.
-
-lemma nlift_flat_sn: ∀W,d,e. (∀V. ⇧[d, e] V ≡ W → ⊥) →
-                     ∀I,U. (∀X. ⇧[d, e] X ≡ ⓕ{I}W.U → ⊥).
-#W #d #e #HW #I #U #X #H elim (lift_inv_flat2 … H) -H /2 width=2 by/
-qed-.
-
-lemma nlift_flat_dx: ∀U,d,e. (∀T. ⇧[d, e] T ≡ U → ⊥) →
-                     ∀I,W. (∀X. ⇧[d, e] X ≡ ⓕ{I}W.U → ⊥).
-#U #d #e #HU #I #W #X #H elim (lift_inv_flat2 … H) -H /2 width=2 by/
-qed-.
-
-(* Inversion lemmas on negated basic relocation *****************************)
-
-lemma nlift_inv_bind: ∀a,I,W,U,d,e. (∀X. ⇧[d, e] X ≡ ⓑ{a,I}W.U → ⊥) →
-                      (∀V. ⇧[d, e] V ≡ W → ⊥) ∨ (∀T. ⇧[d+1, e] T ≡ U → ⊥).
-#a #I #W #U #d #e #H elim (is_lift_dec W d e)
-[ * /4 width=2 by lift_bind, or_intror/
-| /4 width=2 by ex_intro, or_introl/
-]
-qed-.
-
-lemma nlift_inv_flat: ∀I,W,U,d,e. (∀X. ⇧[d, e] X ≡ ⓕ{I}W.U → ⊥) →
-                      (∀V. ⇧[d, e] V ≡ W → ⊥) ∨ (∀T. ⇧[d, e] T ≡ U → ⊥).
-#I #W #U #d #e #H elim (is_lift_dec W d e)
-[ * /4 width=2 by lift_flat, or_intror/
-| /4 width=2 by ex_intro, or_introl/
-]
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_alt.ma
deleted file mode 100644
index ccf131d5a..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_alt.ma
+++ /dev/null
@@ -1,41 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/relocation/llpx_sn_alt.ma".
-include "basic_2/relocation/lleq.ma".
-
-(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
-
-(* Alternative definition ***************************************************)
-
-theorem lleq_intro_alt: ∀L1,L2,T,d. |L1| = |L2| →
-                        (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
-                           ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
-                           ∧∧ I1 = I2 & V1 = V2 & K1 ⋕[V1, 0] K2
-                        ) → L1 ⋕[T, d] L2.
-#L1 #L2 #T #d #HL12 #IH @llpx_sn_intro_alt // -HL12
-#I1 #I2 #K1 #K2 #HLK1 #HLK2 #i #Hid #HnT #HLK1 #HLK2
-elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /2 width=1 by and3_intro/
-qed.
-
-theorem lleq_fwd_alt: ∀L1,L2,T,d. L1 ⋕[T, d] L2 →
-                      |L1| = |L2| ∧
-                      ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
-                      ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
-                      ∧∧ I1 = I2 & V1 = V2 & K1 ⋕[V1, 0] K2.
-#L1 #L2 #T #d #H elim (llpx_sn_fwd_alt … H) -H
-#HL12 #IH @conj //
-#I1 #I2 #K1 #K2 #HLK1 #HLK2 #i #Hid #HnT #HLK1 #HLK2
-elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /2 width=1 by and3_intro/
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn.ma
index 6f1bc4e10..4c4fd5edb 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn.ma
@@ -140,6 +140,11 @@ lemma llpx_sn_fwd_flat_dx: ∀R,I,L1,L2,V,T,d. llpx_sn R d (ⓕ{I}V.T) L1 L2 →
 #R #I #L1 #L2 #V #T #d #H elim (llpx_sn_inv_flat … H) -H //
 qed-.
 
+lemma llpx_sn_fwd_pair_sn: ∀R,I,L1,L2,V,T,d. llpx_sn R d (②{I}V.T) L1 L2 →
+                           llpx_sn R d V L1 L2.
+#R * /2 width=4 by llpx_sn_fwd_flat_sn, llpx_sn_fwd_bind_sn/
+qed-.
+
 (* Basic_properties *********************************************************)
 
 lemma llpx_sn_refl: ∀R. (∀L. reflexive … (R L)) → ∀T,L,d. llpx_sn R d T L L.
@@ -196,3 +201,9 @@ lemma llpx_sn_bind_O: ∀R,a,I,L1,L2,V,T. llpx_sn R 0 V L1 L2 →
                       llpx_sn R 0 T (L1.ⓑ{I}V) (L2.ⓑ{I}V) →
                       llpx_sn R 0 (ⓑ{a,I}V.T) L1 L2.
 /3 width=3 by llpx_sn_ge, llpx_sn_bind/ qed-.
+
+lemma llpx_sn_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) →
+                  ∀L1,L2,T,d. llpx_sn R1 d T L1 L2 → llpx_sn R2 d T L1 L2.
+#R1 #R2 #HR12 #L1 #L2 #T #d #H elim H -L1 -L2 -T -d
+/3 width=9 by llpx_sn_sort, llpx_sn_skip, llpx_sn_lref, llpx_sn_free, llpx_sn_gref, llpx_sn_bind, llpx_sn_flat/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_alt.ma
deleted file mode 100644
index 4356553ff..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_alt.ma
+++ /dev/null
@@ -1,250 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/relocation/lift_neg.ma".
-include "basic_2/relocation/ldrop_ldrop.ma".
-include "basic_2/relocation/llpx_sn.ma".
-
-(* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
-
-(* alternative definition of llpx_sn_alt *)
-inductive llpx_sn_alt (R:relation3 lenv term term): relation4 ynat term lenv lenv ≝
-| llpx_sn_alt_intro: ∀L1,L2,T,d.
-                     (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
-                       ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → I1 = I2 ∧ R K1 V1 V2
-                     ) →
-                     (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
-                       ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → llpx_sn_alt R 0 V1 K1 K2
-                     ) → |L1| = |L2| → llpx_sn_alt R d T L1 L2
-.
-
-(* Basic forward lemmas ******************************************************)
-
-lemma llpx_sn_alt_fwd_gen: ∀R,L1,L2,T,d. llpx_sn_alt R d T L1 L2 →
-                           |L1| = |L2| ∧
-                           ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
-                           ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
-                           ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn_alt R 0 V1 K1 K2.
-#R #L1 #L2 #T #d * -L1 -L2 -T -d
-#L1 #L2 #T #d #IH1 #IH2 #HL12 @conj //
-#I1 #I2 #K1 #K2 #HLK1 #HLK2 #i #Hid #HnT #HLK1 #HLK2
-elim (IH1 … HnT HLK1 HLK2) -IH1 /4 width=8 by and3_intro/
-qed-.
-
-lemma llpx_sn_alt_fwd_length: ∀R,L1,L2,T,d. llpx_sn_alt R d T L1 L2 → |L1| = |L2|.
-#R #L1 #L2 #T #d * -L1 -L2 -T -d //
-qed-.
-
-fact llpx_sn_alt_fwd_lref_aux: ∀R,L1,L2,X,d. llpx_sn_alt R d X L1 L2 → ∀i. X = #i →
-                               ∨∨ |L1| ≤ i ∧ |L2| ≤ i
-                                | yinj i < d
-                                | ∃∃I,K1,K2,V1,V2. ⇩[i] L1 ≡ K1.ⓑ{I}V1 &
-                                                   ⇩[i] L2 ≡ K2.ⓑ{I}V2 &
-                                                   llpx_sn_alt R (yinj 0) V1 K1 K2 &
-                                                   R K1 V1 V2 & d ≤ yinj i.
-#R #L1 #L2 #X #d * -L1 -L2 -X -d
-#L1 #L2 #X #d #H1X #H2X #HL12 #i #H destruct
-elim (lt_or_ge i (|L1|)) /3 width=1 by or3_intro0, conj/
-elim (ylt_split i d) /3 width=1 by or3_intro1/
-#Hdi #HL1 elim (ldrop_O1_lt … HL1) #I1 #K1 #V1 #HLK1
-elim (ldrop_O1_lt L2 i) // #I2 #K2 #V2 #HLK2
-elim (H1X … HLK1 HLK2) -H1X /2 width=3 by nlift_lref_be_SO/ #H #HV12 destruct
-lapply (H2X … HLK1 HLK2) -H2X /2 width=3 by nlift_lref_be_SO/
-/3 width=9 by or3_intro2, ex5_5_intro/
-qed-.
-
-lemma llpx_sn_alt_fwd_lref: ∀R,L1,L2,d,i. llpx_sn_alt R d (#i) L1 L2 →
-                            ∨∨ |L1| ≤ i ∧ |L2| ≤ i
-                             | yinj i < d
-                             | ∃∃I,K1,K2,V1,V2. ⇩[i] L1 ≡ K1.ⓑ{I}V1 &
-                                                ⇩[i] L2 ≡ K2.ⓑ{I}V2 &
-                                                llpx_sn_alt R (yinj 0) V1 K1 K2 &
-                                                R K1 V1 V2 & d ≤ yinj i.
-/2 width=3 by llpx_sn_alt_fwd_lref_aux/ qed-.
-
-(* Basic inversion lemmas ****************************************************)
-
-fact llpx_sn_alt_inv_flat_aux: ∀R,L1,L2,X,d. llpx_sn_alt R d X L1 L2 →
-                               ∀I,V,T. X = ⓕ{I}V.T →
-                               llpx_sn_alt R d V L1 L2 ∧ llpx_sn_alt R d T L1 L2.
-#R #L1 #L2 #X #d * -L1 -L2 -X -d
-#L1 #L2 #X #d #H1X #H2X #HL12
-#I #V #T #H destruct
-@conj @llpx_sn_alt_intro // -HL12
-/4 width=8 by nlift_flat_sn, nlift_flat_dx/
-qed-.
-
-lemma llpx_sn_alt_inv_flat: ∀R,I,L1,L2,V,T,d. llpx_sn_alt R d (ⓕ{I}V.T) L1 L2 →
-                            llpx_sn_alt R d V L1 L2 ∧ llpx_sn_alt R d T L1 L2.
-/2 width=4 by llpx_sn_alt_inv_flat_aux/ qed-.
-
-fact llpx_sn_alt_inv_bind_aux: ∀R,L1,L2,X,d. llpx_sn_alt R d X L1 L2 →
-                               ∀a,I,V,T. X = ⓑ{a,I}V.T →
-                               llpx_sn_alt R d V L1 L2 ∧ llpx_sn_alt R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V).
-#R #L1 #L2 #X #d * -L1 -L2 -X -d
-#L1 #L2 #X #d #H1X #H2X #HL12
-#a #I #V #T #H destruct
-@conj @llpx_sn_alt_intro [3,6: normalize /2 width=1 by eq_f2/ ] -HL12
-#I1 #I2 #K1 #K2 #W1 #W2 #i #Hdi #H #HLK1 #HLK2
-[1,2: /4 width=9 by nlift_bind_sn/ ]
-lapply (yle_inv_succ1 … Hdi) -Hdi * #Hdi #Hi
-lapply (ldrop_inv_drop1_lt … HLK1 ?) -HLK1 /2 width=1 by ylt_O/ #HLK1
-lapply (ldrop_inv_drop1_lt … HLK2 ?) -HLK2 /2 width=1 by ylt_O/ #HLK2
-[ @(H1X … HLK1 HLK2) | @(H2X … HLK1 HLK2) ] // -I1 -I2 -L1 -L2 -K1 -K2 -W1 -W2
-@nlift_bind_dx <plus_minus_m_m /2 width=2 by ylt_O/
-qed-.
-
-lemma llpx_sn_alt_inv_bind: ∀R,a,I,L1,L2,V,T,d. llpx_sn_alt R d (ⓑ{a,I}V.T) L1 L2 →
-                            llpx_sn_alt R d V L1 L2 ∧ llpx_sn_alt R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V).
-/2 width=4 by llpx_sn_alt_inv_bind_aux/ qed-.
-
-(* Basic properties **********************************************************)
-
-lemma llpx_sn_alt_intro_alt: ∀R,L1,L2,T,d. |L1| = |L2| →
-                             (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
-                                ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
-                                ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn_alt R 0 V1 K1 K2
-                             ) → llpx_sn_alt R d T L1 L2.
-#R #L1 #L2 #T #d #HL12 #IH @llpx_sn_alt_intro // -HL12
-#I1 #I2 #K1 #K2 #HLK1 #HLK2 #i #Hid #HnT #HLK1 #HLK2
-elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /2 width=1 by conj/
-qed.
-
-lemma llpx_sn_alt_sort: ∀R,L1,L2,d,k. |L1| = |L2| → llpx_sn_alt R d (⋆k) L1 L2.
-#R #L1 #L2 #d #k #HL12 @llpx_sn_alt_intro // -HL12
-#I1 #I2 #K1 #K2 #V1 #V2 #i #_ #H elim (H (⋆k)) //
-qed.
-
-lemma llpx_sn_alt_gref: ∀R,L1,L2,d,p. |L1| = |L2| → llpx_sn_alt R d (§p) L1 L2.
-#R #L1 #L2 #d #p #HL12 @llpx_sn_alt_intro // -HL12
-#I1 #I2 #K1 #K2 #V1 #V2 #i #_ #H elim (H (§p)) //
-qed.
-
-lemma llpx_sn_alt_skip: ∀R,L1,L2,d,i. |L1| = |L2| → yinj i < d → llpx_sn_alt R d (#i) L1 L2.
-#R #L1 #L2 #d #i #HL12 #Hid @llpx_sn_alt_intro // -HL12
-#I1 #I2 #K1 #K2 #V1 #V2 #j #Hdj #H elim (H (#i)) -H
-/4 width=3 by lift_lref_lt, ylt_yle_trans, ylt_inv_inj/
-qed.
-
-lemma llpx_sn_alt_free: ∀R,L1,L2,d,i. |L1| ≤ i → |L2| ≤ i → |L1| = |L2| →
-                        llpx_sn_alt R d (#i) L1 L2.
-#R #L1 #L2 #d #i #HL1 #_ #HL12 @llpx_sn_alt_intro // -HL12
-#I1 #I2 #K1 #K2 #V1 #V2 #j #_ #H #HLK1 elim (H (#(i-1))) -H
-lapply (ldrop_fwd_length_lt2 … HLK1) -HLK1
-/3 width=3 by lift_lref_ge_minus, lt_to_le_to_lt/
-qed.
-
-lemma llpx_sn_alt_lref: ∀R,I,L1,L2,K1,K2,V1,V2,d,i. d ≤ yinj i →
-                        ⇩[i] L1 ≡ K1.ⓑ{I}V1 → ⇩[i] L2 ≡ K2.ⓑ{I}V2 →
-                        llpx_sn_alt R 0 V1 K1 K2 → R K1 V1 V2 →
-                        llpx_sn_alt R d (#i) L1 L2.
-#R #I #L1 #L2 #K1 #K2 #V1 #V2 #d #i #Hdi #HLK1 #HLK2 #HK12 #HV12 @llpx_sn_alt_intro
-[1,2: #Z1 #Z2 #Y1 #Y2 #X1 #X2 #j #Hdj #H #HLY1 #HLY2
-  elim (lt_or_eq_or_gt i j) #Hij destruct
-  [1,4: elim (H (#i)) -H /2 width=1 by lift_lref_lt/
-  |2,5: lapply (ldrop_mono … HLY1 … HLK1) -HLY1 -HLK1 #H destruct
-    lapply (ldrop_mono … HLY2 … HLK2) -HLY2 -HLK2 #H destruct /2 width=1 by conj/
-  |3,6: elim (H (#(i-1))) -H /2 width=1 by lift_lref_ge_minus/
-  ]
-| lapply (llpx_sn_alt_fwd_length … HK12) -HK12 #HK12
-  @(ldrop_fwd_length_eq2 … HLK1 HLK2) normalize /2 width=1 by eq_f2/
-]
-qed.
-
-fact llpx_sn_alt_flat_aux: ∀R,I,L1,L2,V,d. llpx_sn_alt R d V L1 L2 →
-                           ∀Y1,Y2,T,m. llpx_sn_alt R m T Y1 Y2 →
-                           Y1 = L1 → Y2 = L2 → m = d →
-                           llpx_sn_alt R d (ⓕ{I}V.T) L1 L2.
-#R #I #L1 #L2 #V #d * -L1 -L2 -V -d #L1 #L2 #V #d #H1V #H2V #HL12
-#Y1 #Y2 #T #m * -Y1 -Y2 -T -m #Y1 #Y2 #T #m #H1T #H2T #_
-#HT1 #HY2 #Hm destruct
-@llpx_sn_alt_intro // -HL12
-#J1 #J2 #K1 #K2 #W1 #W2 #i #Hdi #HnVT #HLK1 #HLK2
-elim (nlift_inv_flat … HnVT) -HnVT /3 width=8 by/
-qed-.
-
-lemma llpx_sn_alt_flat: ∀R,I,L1,L2,V,T,d.
-                        llpx_sn_alt R d V L1 L2 → llpx_sn_alt R d T L1 L2 →
-                        llpx_sn_alt R d (ⓕ{I}V.T) L1 L2.
-/2 width=7 by llpx_sn_alt_flat_aux/ qed.
-
-fact llpx_sn_alt_bind_aux: ∀R,a,I,L1,L2,V,d. llpx_sn_alt R d V L1 L2 →
-                           ∀Y1,Y2,T,m. llpx_sn_alt R m T Y1 Y2 →
-                           Y1 = L1.ⓑ{I}V → Y2 = L2.ⓑ{I}V → m = ⫯d →
-                           llpx_sn_alt R d (ⓑ{a,I}V.T) L1 L2.
-#R #a #I #L1 #L2 #V #d * -L1 -L2 -V -d #L1 #L2 #V #d #H1V #H2V #HL12
-#Y1 #Y2 #T #m * -Y1 -Y2 -T -m #Y1 #Y2 #T #m #H1T #H2T #_
-#HT1 #HY2 #Hm destruct
-@llpx_sn_alt_intro // -HL12
-#J1 #J2 #K1 #K2 #W1 #W2 #i #Hdi #HnVT #HLK1 #HLK2
-elim (nlift_inv_bind … HnVT) -HnVT /3 width=8 by ldrop_drop, yle_succ/
-qed-.
-
-lemma llpx_sn_alt_bind: ∀R,a,I,L1,L2,V,T,d.
-                        llpx_sn_alt R d V L1 L2 →
-                        llpx_sn_alt R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) →
-                        llpx_sn_alt R d (ⓑ{a,I}V.T) L1 L2.
-/2 width=7 by llpx_sn_alt_bind_aux/ qed.
-
-(* Main properties **********************************************************)
-
-theorem llpx_sn_lpx_sn_alt: ∀R,L1,L2,T,d. llpx_sn R d T L1 L2 → llpx_sn_alt R d T L1 L2.
-#R #L1 #L2 #T #d #H elim H -L1 -L2 -T -d
-/2 width=9 by llpx_sn_alt_sort, llpx_sn_alt_gref, llpx_sn_alt_skip, llpx_sn_alt_free, llpx_sn_alt_lref, llpx_sn_alt_flat, llpx_sn_alt_bind/
-qed.
-
-(* Main inversion lemmas ****************************************************)
-
-theorem llpx_sn_alt_inv_lpx_sn: ∀R,T,L1,L2,d. llpx_sn_alt R d T L1 L2 → llpx_sn R d T L1 L2.
-#R #T #L1 @(f2_ind … rfw … L1 T) -L1 -T #n #IH #L1 * *
-[1,3: /3 width=4 by llpx_sn_alt_fwd_length, llpx_sn_gref, llpx_sn_sort/
-| #i #Hn #L2 #d #H lapply (llpx_sn_alt_fwd_length … H)
-  #HL12 elim (llpx_sn_alt_fwd_lref … H) -H
-  [ * /2 width=1 by llpx_sn_free/
-  | /2 width=1 by llpx_sn_skip/
-  | * /4 width=9 by llpx_sn_lref, ldrop_fwd_rfw/
-  ]
-| #a #I #V #T #Hn #L2 #d #H elim (llpx_sn_alt_inv_bind … H) -H
-  /3 width=1 by llpx_sn_bind/
-| #I #V #T #Hn #L2 #d #H elim (llpx_sn_alt_inv_flat … H) -H
-  /3 width=1 by llpx_sn_flat/
-]
-qed-.
-
-(* Advanced properties ******************************************************)
-
-lemma llpx_sn_intro_alt: ∀R,L1,L2,T,d. |L1| = |L2| →
-                         (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
-                            ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
-                            ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn R 0 V1 K1 K2
-                         ) → llpx_sn R d T L1 L2.
-#R #L1 #L2 #T #d #HL12 #IH @llpx_sn_alt_inv_lpx_sn
-@llpx_sn_alt_intro_alt // -HL12
-#I1 #I2 #K1 #K2 #HLK1 #HLK2 #i #Hid #HnT #HLK1 #HLK2
-elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /3 width=1 by llpx_sn_lpx_sn_alt, and3_intro/
-qed.
-
-(* Advanced forward lemmas lemmas *******************************************)
-
-lemma llpx_sn_fwd_alt: ∀R,L1,L2,T,d. llpx_sn R d T L1 L2 →
-                       |L1| = |L2| ∧
-                       ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
-                       ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
-                       ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn R 0 V1 K1 K2.
-#R #L1 #L2 #T #d #H lapply (llpx_sn_lpx_sn_alt … H) -H
-#H elim (llpx_sn_alt_fwd_gen … H) -H
-#HL12 #IH @conj //
-#I1 #I2 #K1 #K2 #HLK1 #HLK2 #i #Hid #HnT #HLK1 #HLK2
-elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /3 width=1 by llpx_sn_alt_inv_lpx_sn, and3_intro/
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_ldrop.ma
index 4d90e2332..49ee69f7c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_ldrop.ma
@@ -386,6 +386,27 @@ lemma llpx_sn_inv_lift_ge: ∀R,L1,L2,U,d0. llpx_sn R d0 U L1 L2 →
 ]
 qed-.
 
+(* Advanced inversion lemmas on relocation **********************************)
+
+lemma llpx_sn_inv_lift_O: ∀R,L1,L2,U. llpx_sn R 0 U L1 L2 →
+                          ∀K1,K2,e. ⇩[e] L1 ≡ K1 → ⇩[e] L2 ≡ K2 →
+                          ∀T. ⇧[0, e] T ≡ U → llpx_sn R 0 T K1 K2.
+/2 width=11 by llpx_sn_inv_lift_be/ qed-.
+
+lemma llpx_sn_ldrop_conf_O: ∀R,L1,L2,U. llpx_sn R 0 U L1 L2 →
+                            ∀K1,e. ⇩[e] L1 ≡ K1 → ∀T. ⇧[0, e] T ≡ U →
+                            ∃∃K2. ⇩[e] L2 ≡ K2 & llpx_sn R 0 T K1 K2.
+#R #L1 #L2 #U #HU #K1 #e #HLK1 #T #HTU elim (llpx_sn_fwd_ldrop_sn … HU … HLK1)
+/3 width=10 by llpx_sn_inv_lift_O, ex2_intro/
+qed-.
+
+lemma llpx_sn_ldrop_trans_O: ∀R,L1,L2,U. llpx_sn R 0 U L1 L2 →
+                             ∀K2,e. ⇩[e] L2 ≡ K2 → ∀T. ⇧[0, e] T ≡ U →
+                             ∃∃K1. ⇩[e] L1 ≡ K1 & llpx_sn R 0 T K1 K2.
+#R #L1 #L2 #U #HU #K2 #e #HLK2 #T #HTU elim (llpx_sn_fwd_ldrop_dx … HU … HLK2)
+/3 width=10 by llpx_sn_inv_lift_O, ex2_intro/
+qed-.
+
 (* Inversion lemmas on negated lazy pointwise extension *********************)
 
 lemma nllpx_sn_inv_bind: ∀R. (∀L,T1,T2. Decidable (R L T1 T2)) →
diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
index b3efe3bc3..cb5bedd59 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -137,7 +137,7 @@ table {
         ]
         [ { "context-sensitive extended reduction" * } {
              [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_ldrop" + "lpx_lleq" + "lpx_aaa" * ]
-             [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_leq" + "cpx_lift" + "cpx_lleq" + "cpx_cix" * ]
+             [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_leq" + "cpx_lift" + "cpx_llpx_sn" + "cpx_lleq" + "cpx_cix" * ]
           }
         ]
         [ { "irreducible forms for context-sensitive extended reduction" * } {
@@ -245,11 +245,11 @@ table {
           }
         ]
         [ { "lazy equivalence for local environments" * } {
-             [ "lleq ( ? ⋕[?,?] ? )" "lleq_alt" + "lleq_leq" + "lleq_ldrop" + "lleq_lleq" * ]
+             [ "lleq ( ? ⋕[?,?] ? )" "lleq_leq" + "lleq_ldrop" + "lleq_lleq" * ]
           }
         ]
         [ { "lazy pointwise extension of a relation" * } {
-             [ "llpx_sn" "llpx_sn_alt" + "llpx_sn_leq" + "llpx_sn_ldrop" * ]
+             [ "llpx_sn" "llpx_sn_leq" + "llpx_sn_ldrop" + "llpx_sn_llpx_sn" * ]
           }
         ]        
 	[ { "basic local env. slicing" * } {
@@ -258,7 +258,7 @@ table {
         ]
         [ { "basic term relocation" * } {
              [ "lift_vector ( ⇧[?,?] ? ≡ ? )" "lift_lift_vector" * ]
-             [ "lift ( ⇧[?,?] ? ≡ ? )" "lift_neg" + "lift_lift" * ]
+             [ "lift ( ⇧[?,?] ? ≡ ? )" "lift_lift" * ]
           }
         ]
      }