From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 26 Dec 2013 14:54:55 +0000 (+0000)
Subject: the theory of extended multiple substitution for therms is complete
X-Git-Tag: make_still_working~1010
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e76eade57c0454a58b0d58e5484efe9af417847e;p=helm.git

the theory of extended multiple substitution for therms is complete
a simpler theory is complete as well but parked in etc for now
---

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
index efa8e3da6..640f4dbfc 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
@@ -60,7 +60,7 @@ lemma cprs_strap2: ∀G,L,T1,T,T2.
 normalize /2 width=3/ qed.
 
 lemma lsubr_cprs_trans: ∀G. lsub_trans … (cprs G) lsubr.
-/3 width=5 by lsubr_cpr_trans, TC_lsub_trans/
+/3 width=5 by lsubr_cpr_trans, LTC_lsub_trans/
 qed-.
 
 (* Basic_1: was: pr3_pr1 *)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma
index 91ddd1621..a3f8e8316 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma
@@ -57,7 +57,7 @@ lemma cpxs_strap2: ∀h,g,G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡[h, g] T →
 normalize /2 width=3 by TC_strap/ qed.
 
 lemma lsubr_cpxs_trans: ∀h,g,G. lsub_trans … (cpxs h g G) lsubr.
-/3 width=5 by lsubr_cpx_trans, TC_lsub_trans/
+/3 width=5 by lsubr_cpx_trans, LTC_lsub_trans/
 qed-.
 
 lemma cprs_cpxs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/cpys.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/cpys.etc
new file mode 100644
index 000000000..a0603f13e
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/cpys.etc
@@ -0,0 +1,200 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/extpsubststar_4.ma".
+include "basic_2/grammar/genv.ma".
+include "basic_2/grammar/cl_shift.ma".
+include "basic_2/relocation/ldrop_append.ma".
+include "basic_2/relocation/lsuby.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED MULTIPLE SUBSTITUTION FOR TERMS ***************)
+
+(* avtivate genv *)
+inductive cpys: relation4 genv lenv term term ≝
+| cpys_atom : ∀I,G,L. cpys G L (⓪{I}) (⓪{I})
+| cpys_delta: ∀I,G,L,K,V,V2,W2,i.
+              ⇩[0, i] L ≡ K.ⓑ{I}V → cpys G K V V2 →
+              ⇧[0, i + 1] V2 ≡ W2 → cpys G L (#i) W2
+| cpys_bind : ∀a,I,G,L,V1,V2,T1,T2.
+              cpys G L V1 V2 → cpys G (L.ⓑ{I}V1) T1 T2 →
+              cpys G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
+| cpys_flat : ∀I,G,L,V1,V2,T1,T2.
+              cpys G L V1 V2 → cpys G L T1 T2 →
+              cpys G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
+.
+
+interpretation
+   "context-sensitive extended multiple substitution (term)"
+   'ExtPSubstStar G L T1 T2 = (cpys G L T1 T2).
+
+(* Basic properties *********************************************************)
+
+lemma lsuby_cpys_trans: ∀G. lsub_trans … (cpys G) lsuby.
+#G #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2
+[ //
+| #I #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
+  elim (lsuby_fwd_ldrop2_pair … HL12 … HLK1) -HL12 -HLK1 *
+  /3 width=7 by cpys_delta/
+| /4 width=1 by lsuby_pair, cpys_bind/
+| /3 width=1 by cpys_flat/
+]
+qed-.
+
+(* Note: this is "∀L. reflexive … (cpys L)" *)
+lemma cpys_refl: ∀G,T,L. ⦃G, L⦄ ⊢ T ▶*× T.
+#G #T elim T -T // * /2 width=1 by cpys_bind, cpys_flat/
+qed.
+
+lemma cpys_pair_sn: ∀I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ▶*× V2 →
+                    ∀T. ⦃G, L⦄ ⊢ ②{I}V1.T ▶*× ②{I}V2.T.
+* /2 width=1 by cpys_bind, cpys_flat/
+qed.
+
+lemma cpys_bind_ext: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ▶*× V2 →
+                     ∀J,T1,T2. ⦃G, L.ⓑ{J}V1⦄ ⊢ T1 ▶*× T2 →
+                     ∀a,I. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*× ⓑ{a,I}V2.T2.
+/4 width=4 by lsuby_cpys_trans, cpys_bind, lsuby_pair/ qed.
+
+lemma cpys_delift: ∀I,G,K,V,T1,L,d. ⇩[0, d] L ≡ (K.ⓑ{I}V) →
+                   ∃∃T2,T.  ⦃G, L⦄ ⊢ T1 ▶*× T2 & ⇧[d, 1] T ≡ T2.
+#I #G #K #V #T1 elim T1 -T1
+[ * /2 width=4 by cpys_atom, lift_sort, lift_gref, ex2_2_intro/
+  #i #L #d elim (lt_or_eq_or_gt i d) #Hid [1,3: /3 width=4 by cpys_atom, lift_lref_ge_minus, lift_lref_lt, ex2_2_intro/ ]
+  destruct
+  elim (lift_total V 0 (i+1)) #W #HVW
+  elim (lift_split … HVW i i) /3 width=7 by cpys_delta, ex2_2_intro/
+| * [ #a ] #I #W1 #U1 #IHW1 #IHU1 #L #d #HLK
+  elim (IHW1 … HLK) -IHW1 #W2 #W #HW12 #HW2
+  [ elim (IHU1 (L. ⓑ{I}W1) (d+1)) -IHU1 /3 width=9 by cpys_bind, ldrop_ldrop, lift_bind, ex2_2_intro/
+  | elim (IHU1 … HLK) -IHU1 -HLK /3 width=8 by cpys_flat, lift_flat, ex2_2_intro/
+  ]
+]
+qed-.
+
+lemma cpys_append: ∀G. l_appendable_sn … (cpys G).
+#G #K #T1 #T2 #H elim H -G -K -T1 -T2
+/2 width=3 by cpys_bind, cpys_flat/
+#I #G #K #K0 #V1 #V2 #W2 #i #HK0 #_ #HVW2 #IHV12 #L
+lapply (ldrop_fwd_length_lt2 … HK0) #H
+@(cpys_delta … I … (L@@K0) V1 … HVW2) // 
+@(ldrop_O1_append_sn_le … HK0) /2 width=2 by lt_to_le/ (**) (* /3/ does not work *)
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact cpys_inv_atom1_aux: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ▶*× T2 → ∀J. T1 = ⓪{J} →
+                         T2 = ⓪{J} ∨
+                         ∃∃I,K,V,V2,i. ⇩[O, i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ▶*× V2 &
+                                       ⇧[O, i + 1] V2 ≡ T2 & J = LRef i.
+#G #L #T1 #T2 * -L -T1 -T2
+[ #I #G #L #J #H destruct /2 width=1 by or_introl/
+| #I #G #L #K #V #V2 #T2 #i #HLK #HV2 #HVT2 #J #H destruct /3 width=9 by ex4_5_intro, or_intror/
+| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
+| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
+]
+qed-.
+
+lemma cpys_inv_atom1: ∀J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ▶*× T2 →
+                      T2 = ⓪{J} ∨
+                      ∃∃I,K,V,V2,i. ⇩[O, i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ▶*× V2 &
+                                    ⇧[O, i + 1] V2 ≡ T2 & J = LRef i.
+/2 width=3 by cpys_inv_atom1_aux/ qed-.
+
+lemma cpys_inv_sort1: ∀G,L,T2,k. ⦃G, L⦄ ⊢ ⋆k ▶*× T2 → T2 = ⋆k.
+#G #L #T2 #k #H elim (cpys_inv_atom1 … H) -H // *
+#I #K #V #V2 #i #_ #_ #_ #H destruct
+qed-.
+
+lemma cpys_inv_lref1: ∀G,L,T2,i. ⦃G, L⦄ ⊢ #i ▶*× T2 →
+                      T2 = #i ∨
+                      ∃∃I,K,V,V2. ⇩[O, i] L ≡ K. ⓑ{I}V & ⦃G, K⦄ ⊢ V ▶*× V2 &
+                                  ⇧[O, i + 1] V2 ≡ T2.
+#G #L #T2 #i #H elim (cpys_inv_atom1 … H) -H /2 width=1 by or_introl/ *
+#I #K #V #V2 #j #HLK #HV2 #HVT2 #H destruct /3 width=7 by ex3_4_intro, or_intror/
+qed-.
+
+lemma cpys_inv_lref1_ge: ∀G,L,T2,i. ⦃G, L⦄ ⊢ #i ▶*× T2 → |L| ≤ i → T2 = #i.
+#G #L #T2 #i #H elim (cpys_inv_lref1 … H) -H // *
+#I #K #V1 #V2 #HLK #_ #_ #HL -V2 lapply (ldrop_fwd_length_lt2 … HLK) -K -I -V1
+#H elim (lt_refl_false i) /2 width=3 by lt_to_le_to_lt/
+qed-.
+
+lemma cpys_inv_gref1: ∀G,L,T2,p.  ⦃G, L⦄ ⊢ §p ▶*× T2 → T2 = §p.
+#G #L #T2 #p #H elim (cpys_inv_atom1 … H) -H // *
+#I #K #V #V2 #i #_ #_ #_ #H destruct
+qed-.
+
+fact cpys_inv_bind1_aux: ∀G,L,U1,U2. ⦃G, L⦄ ⊢ U1 ▶*× U2 →
+                         ∀a,J,V1,T1. U1 = ⓑ{a,J}V1.T1 →
+                         ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*× V2 & ⦃G, L.ⓑ{J}V1⦄ ⊢ T1 ▶*× T2 &
+                                  U2 = ⓑ{a,J}V2.T2.
+#G #L #U1 #U2 * -L -U1 -U2
+[ #I #G #L #b #J #W #U1 #H destruct
+| #I #G #L #K #V #V2 #W2 #i #_ #_ #_ #b #J #W #U1 #H destruct
+| #a #I #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #b #J #W #U1 #H destruct /2 width=5 by ex3_2_intro/
+| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #b #J #W #U1 #H destruct
+]
+qed-.
+
+lemma cpys_inv_bind1: ∀a,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*× U2 →
+                      ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*× V2 & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶*× T2 &
+                               U2 = ⓑ{a,I}V2.T2.
+/2 width=3 by cpys_inv_bind1_aux/ qed-.
+
+lemma cpys_inv_bind1_ext: ∀a,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*× U2 → ∀J.
+                          ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*× V2 & ⦃G, L.ⓑ{J}V1⦄ ⊢ T1 ▶*× T2 &
+                                   U2 = ⓑ{a,I}V2.T2.
+#a #I #G #L #V1 #T1 #U2 #H #J elim (cpys_inv_bind1 … H) -H
+#V2 #T2 #HV12 #HT12 #H destruct
+/4 width=5 by lsuby_cpys_trans, lsuby_pair, ex3_2_intro/
+qed-.
+
+fact cpys_inv_flat1_aux: ∀G,L,U,U2. ⦃G, L⦄ ⊢ U ▶*× U2 →
+                         ∀J,V1,U1. U = ⓕ{J}V1.U1 →
+                         ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*× V2 & ⦃G, L⦄ ⊢ U1 ▶*× T2 &
+                                  U2 = ⓕ{J}V2.T2.
+#G #L #U #U2 * -L -U -U2
+[ #I #G #L #J #W #U1 #H destruct
+| #I #G #L #K #V #V2 #W2 #i #_ #_ #_ #J #W #U1 #H destruct
+| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #J #W #U1 #H destruct
+| #I #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #J #W #U1 #H destruct /2 width=5 by ex3_2_intro/
+]
+qed-.
+
+lemma cpys_inv_flat1: ∀I,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓕ{I}V1.U1 ▶*× U2 →
+                      ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*× V2 & ⦃G, L⦄ ⊢ U1 ▶*× T2 &
+                               U2 = ⓕ{I}V2.T2.
+/2 width=3 by cpys_inv_flat1_aux/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma cpys_fwd_bind1: ∀a,I,G,L,V1,T1,T. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*× T → ∀b,J.
+                      ∃∃V2,T2. ⦃G, L⦄ ⊢ ⓑ{b,J}V1.T1 ▶*× ⓑ{b,J}V2.T2 &
+                               T = ⓑ{a,I}V2.T2.
+#a #I #G #L #V1 #T1 #T #H #b #J elim (cpys_inv_bind1_ext … H J) -H
+#V2 #T2 #HV12 #HT12 #H destruct /3 width=4 by cpys_bind, ex2_2_intro/
+qed-.
+
+lemma cpys_fwd_shift1: ∀G,L1,L,T1,T. ⦃G, L⦄ ⊢ L1 @@ T1 ▶*× T →
+                       ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2.
+#G #L1 @(lenv_ind_dx … L1) -L1 normalize
+[ #L #T1 #T #HT1 @(ex2_2_intro … (⋆)) // (**) (* explicit constructor *)
+| #I #L1 #V1 #IH #L #T1 #X >shift_append_assoc normalize
+  #H elim (cpys_inv_bind1 … H) -H
+  #V0 #T0 #_ #HT10 #H destruct
+  elim (IH … HT10) -IH -HT10 #L2 #T2 #HL12 #H destruct
+  >append_length >HL12 -HL12
+  @(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] /2 width=3 by trans_eq/ (**) (* explicit constructor *)
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/cpys_cpys.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/cpys_cpys.etc
new file mode 100644
index 000000000..e0abed64d
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/cpys_cpys.etc
@@ -0,0 +1,72 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/grammar/lpx_sn_lpx_sn.ma".
+include "basic_2/substitution/fqup.ma".
+include "basic_2/substitution/lpys_ldrop.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED MULTIPLE SUBSTITUTION FOR TERMS ***************)
+
+(* Main properties **********************************************************)
+
+theorem cpys_antisym: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ▶*× T2 → ⦃G, L⦄ ⊢ T2 ▶*× T1 → T1 = T2.
+#G #L #T1 #T2 #H elim H -G -L -T1 -T2 //
+[ #I #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #_ #HW2 lapply (ldrop_fwd_ldrop2 … HLK) -I -V1
+  #HLK elim (cpys_inv_lift1 … HW2 … HLK … HVW2) -L -HVW2
+  #X #H #_ elim (lift_inv_lref2_be … H) -G -K -V2 -W2 -X //
+| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #H elim (cpys_inv_bind1 … H) -H
+  #V #T #HV2 #HT2 #H destruct
+  lapply (IHV12 HV2) #H destruct -IHV12 -HV2 /3 width=1 by eq_f2/
+| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #H elim (cpys_inv_flat1 … H) -H
+  #V #T #HV2 #HT2 #H destruct /3 width=1 by eq_f2/
+]
+qed-.
+
+theorem cpys_trans_lpys: ∀G. lpx_sn_transitive (cpys G) (cpys G).
+#G0 #L0 #T0 @(fqup_wf_ind_eq … G0 L0 T0) -G0 -L0 -T0 #G0 #L0 #T0 #IH #G1 #L1 * [|*]
+[ #I #HG #HL #HT #T #H1 #L2 #HL12 #T2 #HT2 destruct
+  elim (cpys_inv_atom1 … H1) -H1
+  [ #H destruct
+    elim (cpys_inv_atom1 … HT2) -HT2
+    [ #H destruct //
+    | * #I2 #K2 #V #V2 #i #HLK2 #HV2 #HVT2 #H destruct
+      elim (lpys_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
+      elim (lpys_inv_pair2 … H) -H #K1 #V1 #HK12 #HV1 #H destruct
+      lapply (fqup_lref … G1 … HLK1) /3 width=10 by cpys_delta/
+    ]
+  | * #I1 #K1 #V1 #V #i #HLK1 #HV1 #HVT #H destruct
+    elim (lpys_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
+    elim (lpys_inv_pair1 … H) -H #K2 #W2 #HK12 #_ #H destruct
+    lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2
+    elim (cpys_inv_lift1 … HT2 … HLK2 … HVT) -L2 -T
+    lapply (fqup_lref … G1 … HLK1) /3 width=10 by cpys_delta/
+  ]
+| #a #I #V1 #T1 #HG #HL #HT #X1 #H1 #L2 #HL12 #X2 #H2
+  elim (cpys_inv_bind1 … H1) -H1 #V #T #HV1 #HT1 #H destruct
+  elim (cpys_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct
+  /4 width=5 by cpys_bind, lpys_pair/
+| #I #V1 #T1 #HG #HL #HT #X1 #H1 #L2 #HL12 #X2 #H2
+  elim (cpys_inv_flat1 … H1) -H1 #V #T #HV1 #HT1 #H destruct
+  elim (cpys_inv_flat1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct
+  /3 width=5 by cpys_flat/
+]
+qed-.
+
+theorem cpys_trans: ∀G,L. Transitive … (cpys G L).
+/2 width=5 by cpys_trans_lpys/ qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma lpys_cpys_trans: ∀G. lsub_trans … (cpys G) (lpys G).
+/2 width=5 by cpys_trans_lpys/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/cpys_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/cpys_lift.etc
new file mode 100644
index 000000000..d798c8a62
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/cpys_lift.etc
@@ -0,0 +1,176 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/ldrop_ldrop.ma".
+include "basic_2/substitution/fqus_alt.ma".
+include "basic_2/substitution/cpys.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED MULTIPLE SUBSTITUTION FOR TERMS ***************)
+
+(* Relocation properties ****************************************************)
+
+lemma cpys_lift: ∀G. l_liftable (cpys G).
+#G #K #T1 #T2 #H elim H -G -K -T1 -T2
+[ #I #G #K #L #d #e #_ #U1 #H1 #U2 #H2
+  >(lift_mono … H1 … H2) -H1 -H2 //
+| #I #G #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #d #e #HLK #U1 #H #U2 #HWU2
+  elim (lift_inv_lref1 … H) * #Hid #H destruct
+  [ elim (lift_trans_ge … HVW2 … HWU2) -W2 // <minus_plus #W2 #HVW2 #HWU2
+    elim (ldrop_trans_le … HLK … HKV) -K /2 width=2 by lt_to_le/ #X #HLK #H
+    elim (ldrop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hid #K #Y #HKV #HVY #H destruct /3 width=9 by cpys_delta/
+  | lapply (lift_trans_be … HVW2 … HWU2 ? ?) -W2 /2 width=1 by le_S/ >plus_plus_comm_23 #HVU2
+    lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K /3 width=7 by cpys_delta/
+  ]
+| #a #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2
+  elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct
+  elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /4 width=5 by cpys_bind, ldrop_skip/
+| #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2
+  elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct
+  elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /3 width=6 by cpys_flat/
+]
+qed.
+
+lemma cpys_inv_lift1: ∀G. l_deliftable_sn (cpys G).
+#G #L #U1 #U2 #H elim H -G -L -U1 -U2
+[ * #G #L #i #K #d #e #_ #T1 #H
+  [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by cpys_atom, lift_sort, ex2_intro/
+  | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by cpys_atom, lift_lref_ge_minus, lift_lref_lt, ex2_intro/
+  | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by cpys_atom, lift_gref, ex2_intro/
+  ]
+| #I #G #L #LV #V #V2 #W2 #i #HLV #HV2 #HVW2 #IHV2 #K #d #e #HLK #T1 #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 cpys_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 cpys_delta, ex2_intro/
+  ]
+| #a #I #G #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #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=5 by cpys_bind, ldrop_skip, lift_bind, ex2_intro/
+| #I #G #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #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 cpys_flat, lift_flat, ex2_intro/
+]
+qed-.
+
+(* Properties on supclosure *************************************************)
+
+lemma fqu_cpys_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
+                      ∀U2. ⦃G2, L2⦄ ⊢ T2 ▶*× U2 →
+                      ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ▶*× U1 & ⦃G1, L1, U1⦄ ⊃ ⦃G2, L2, U2⦄.
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 
+/3 width=3 by fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, cpys_pair_sn, cpys_bind, cpys_flat, ex2_intro/
+[ #I #G #L #V2 #U2 #HVU2
+  elim (lift_total U2 0 1)
+  /4 width=7 by fqu_drop, cpys_delta, ldrop_pair, ldrop_ldrop, ex2_intro/
+| #G #L #K #T1 #U1 #e #HLK1 #HTU1 #T2 #HTU2
+  elim (lift_total T2 0 (e+1))
+  /3 width=11 by cpys_lift, fqu_drop, ex2_intro/
+]
+qed-.
+
+lemma fquq_cpys_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+                       ∀U2. ⦃G2, L2⦄ ⊢ T2 ▶*× U2 →
+                       ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ▶*× U1 & ⦃G1, L1, U1⦄ ⊃⸮ ⦃G2, L2, U2⦄.
+#G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 elim (fquq_inv_gen … H) -H
+[ #HT12 elim (fqu_cpys_trans … HT12 … HTU2) /3 width=3 by fqu_fquq, ex2_intro/
+| * #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/
+]
+qed-.
+
+lemma fqup_cpys_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
+                       ∀U2. ⦃G2, L2⦄ ⊢ T2 ▶*× U2 →
+                       ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ▶*× U1 & ⦃G1, L1, U1⦄ ⊃+ ⦃G2, L2, U2⦄.
+#G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
+[ #G2 #L2 #T2 #H12 #U2 #HTU2 elim (fqu_cpys_trans … H12 … HTU2) -T2
+  /3 width=3 by fqu_fqup, ex2_intro/
+| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #U2 #HTU2
+  elim (fqu_cpys_trans … HT2 … HTU2) -T2 #T2 #HT2 #HTU2
+  elim (IHT1 … HT2) -T /3 width=7 by fqup_strap1, ex2_intro/
+]
+qed-.
+
+lemma fqus_cpys_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
+                       ∀U2. ⦃G2, L2⦄ ⊢ T2 ▶*× U2 →
+                       ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ▶*× U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄.
+#G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 elim (fqus_inv_gen … H) -H
+[ #HT12 elim (fqup_cpys_trans … HT12 … HTU2) /3 width=3 by fqup_fqus, ex2_intro/
+| * #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/
+]
+qed-.
+
+lemma fqu_cpys_trans_neq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
+                          ∀U2. ⦃G2, L2⦄ ⊢ T2 ▶*× U2 → (T2 = U2 → ⊥) →
+                          ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ▶*× U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊃ ⦃G2, L2, U2⦄.
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+[ #I #G #L #V1 #V2 #HV12 #_ elim (lift_total V2 0 1)
+  #U2 #HVU2 @(ex3_intro … U2)
+  [1,3: /3 width=7 by fqu_drop, cpys_delta, ldrop_pair, ldrop_ldrop/
+  | #H destruct /2 width=7 by lift_inv_lref2_be/
+  ]
+| #I #G #L #V1 #T #V2 #HV12 #H @(ex3_intro … (②{I}V2.T))
+  [1,3: /2 width=4 by fqu_pair_sn, cpys_pair_sn/
+  | #H0 destruct /2 width=1 by/
+  ]
+| #a #I #G #L #V #T1 #T2 #HT12 #H @(ex3_intro … (ⓑ{a,I}V.T2))
+  [1,3: /2 width=4 by fqu_bind_dx, cpys_bind/
+  | #H0 destruct /2 width=1 by/
+  ]
+| #I #G #L #V #T1 #T2 #HT12 #H @(ex3_intro … (ⓕ{I}V.T2))
+  [1,3: /2 width=4 by fqu_flat_dx, cpys_flat/
+  | #H0 destruct /2 width=1 by/
+  ]
+| #G #L #K #T1 #U1 #e #HLK #HTU1 #T2 #HT12 #H elim (lift_total T2 0 (e+1))
+  #U2 #HTU2 @(ex3_intro … U2)
+  [1,3: /2 width=9 by cpys_lift, fqu_drop/
+  | #H0 destruct /3 width=5 by lift_inj/
+]
+qed-.
+
+lemma fquq_cpys_trans_neq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+                           ∀U2. ⦃G2, L2⦄ ⊢ T2 ▶*× U2 → (T2 = U2 → ⊥) →
+                           ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ▶*× U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊃⸮ ⦃G2, L2, U2⦄.
+#G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fquq_inv_gen … H12) -H12
+[ #H12 elim (fqu_cpys_trans_neq … H12 … HTU2 H) -T2
+  /3 width=4 by fqu_fquq, ex3_intro/
+| * #HG #HL #HT destruct /3 width=4 by ex3_intro/
+]
+qed-.
+
+lemma fqup_cpys_trans_neq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
+                           ∀U2. ⦃G2, L2⦄ ⊢ T2 ▶*× U2 → (T2 = U2 → ⊥) →
+                           ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ▶*× U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊃+ ⦃G2, L2, U2⦄.
+#G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind_dx … H) -G1 -L1 -T1
+[ #G1 #L1 #T1 #H12 #U2 #HTU2 #H elim (fqu_cpys_trans_neq … H12 … HTU2 H) -T2
+  /3 width=4 by fqu_fqup, ex3_intro/
+| #G #G1 #L #L1 #T #T1 #H1 #_ #IH12 #U2 #HTU2 #H elim (IH12 … HTU2 H) -T2
+  #U1 #HTU1 #H #H12 elim (fqu_cpys_trans_neq … H1 … HTU1 H) -T1
+  /3 width=8 by fqup_strap2, ex3_intro/
+]
+qed-.
+
+lemma fqus_cpys_trans_neq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
+                           ∀U2. ⦃G2, L2⦄ ⊢ T2 ▶*× U2 → (T2 = U2 → ⊥) →
+                           ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ▶*× U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄.
+#G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fqus_inv_gen … H12) -H12
+[ #H12 elim (fqup_cpys_trans_neq … H12 … HTU2 H) -T2
+  /3 width=4 by fqup_fqus, ex3_intro/
+| * #HG #HL #HT destruct /3 width=4 by ex3_intro/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/extlrsubeq_2.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/extlrsubeq_2.etc
new file mode 100644
index 000000000..97bdb1828
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/extlrsubeq_2.etc
@@ -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( L1 break ⊑ × break term 46 L2 )"
+   non associative with precedence 45
+   for @{ 'ExtLRSubEq $L1 $L2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/extpsubstsnstar_3.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/extpsubstsnstar_3.etc
new file mode 100644
index 000000000..64acfff4c
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/extpsubstsnstar_3.etc
@@ -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 L2 )"
+   non associative with precedence 45
+   for @{ 'ExtPSubstSnStar $G $L1 $L2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/extpsubststar_4.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/extpsubststar_4.etc
new file mode 100644
index 000000000..363dce487
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/extpsubststar_4.etc
@@ -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 L ⦄ ⊢ break term 46 T1 break ▶ * × break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'ExtPSubstStar $G $L $T1 $T2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/lpys.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/lpys.etc
new file mode 100644
index 000000000..083fbbe46
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/lpys.etc
@@ -0,0 +1,75 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/extpsubstsnstar_3.ma".
+include "basic_2/grammar/lpx_sn.ma".
+include "basic_2/substitution/cpys.ma".
+
+(* SN EXTENDED MULTIPLE SUBSTITUTION FOR LOCAL ENVIRONMENTS *****************)
+
+definition lpys: relation3 genv lenv lenv ≝ λG. lpx_sn (cpys G).
+
+interpretation
+   "extended multiple substitution (local environment, sn variant)"
+   'ExtPSubstSnStar G L1 L2 = (lpys G L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lpys_inv_atom1: ∀G,L2. ⦃G, ⋆⦄ ⊢ ▶*× L2 → L2 = ⋆.
+/2 width=4 by lpx_sn_inv_atom1_aux/ qed-.
+
+lemma lpys_inv_pair1: ∀I,G,K1,V1,L2. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ▶*× L2 →
+                      ∃∃K2,V2. ⦃G, K1⦄ ⊢ ▶*× K2 & ⦃G, K1⦄ ⊢ V1 ▶*× V2 &
+                               L2 = K2. ⓑ{I} V2.
+/2 width=3 by lpx_sn_inv_pair1_aux/ qed-.
+
+lemma lpys_inv_atom2: ∀G,L1. ⦃G, L1⦄ ⊢ ▶*× ⋆ → L1 = ⋆.
+/2 width=4 by lpx_sn_inv_atom2_aux/ qed-.
+
+lemma lpys_inv_pair2: ∀I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ▶*× K2.ⓑ{I}V2 →
+                      ∃∃K1,V1. ⦃G, K1⦄ ⊢ ▶*× K2 & ⦃G, K1⦄ ⊢ V1 ▶*× V2 &
+                               L1 = K1. ⓑ{I} V1.
+/2 width=3 by lpx_sn_inv_pair2_aux/ qed-.
+
+lemma lpys_inv_pair: ∀I1,I2,G,L1,L2,V1,V2. ⦃G, L1.ⓑ{I1}V1⦄ ⊢ ▶*× L2.ⓑ{I2}V2 →
+                     ∧∧ ⦃G, L1⦄ ⊢ ▶*× L2 & ⦃G, L1⦄ ⊢ V1 ▶*× V2 & I1 = I2.
+/2 width=1 by lpx_sn_inv_pair/ qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lpys_refl: ∀G,L. ⦃G, L⦄ ⊢ ▶*× L.
+/2 width=1 by lpx_sn_refl/ qed.
+
+lemma lpys_pair: ∀I,G,K1,K2,V1,V2. ⦃G, K1⦄ ⊢ ▶*× K2 → ⦃G, K1⦄ ⊢ V1 ▶*× V2 →
+                 ⦃G, K1.ⓑ{I}V1⦄ ⊢ ▶*× K2.ⓑ{I}V2.
+/2 width=1 by lpx_sn_pair/ qed.
+
+lemma lpys_append: ∀G,K1,K2. ⦃G, K1⦄ ⊢ ▶*× K2 → ∀L1,L2. ⦃G, L1⦄ ⊢ ▶*× L2 →
+                   ⦃G, L1 @@ K1⦄ ⊢ ▶*× L2 @@ K2.
+/3 width=1 by lpx_sn_append, cpys_append/ qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lpys_fwd_length: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ▶*× L2 → |L1| = |L2|.
+/2 width=2 by lpx_sn_fwd_length/ qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma lpys_fwd_append1: ∀G,K1,L1,L. ⦃G, K1 @@ L1⦄ ⊢ ▶*× L →
+                        ∃∃K2,L2. ⦃G, K1⦄ ⊢ ▶*× K2 & L = K2 @@ L2.
+/2 width=2 by lpx_sn_fwd_append1/ qed-.
+
+lemma lpys_fwd_append2: ∀G,L,K2,L2. ⦃G, L⦄ ⊢ ▶*× K2 @@ L2 →
+                        ∃∃K1,L1. ⦃G, K1⦄ ⊢ ▶*× K2 & L = K1 @@ L1.
+/2 width=2 by lpx_sn_fwd_append2/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/lpys_ldrop.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/lpys_ldrop.etc
new file mode 100644
index 000000000..df77274de
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/lpys_ldrop.etc
@@ -0,0 +1,78 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/ldrop_lpx_sn.ma".
+include "basic_2/substitution/cpys_lift.ma".
+include "basic_2/substitution/lpys.ma".
+
+(* SN EXTENDED MULTIPLE SUBSTITUTION FOR LOCAL ENVIRONMENTS *****************)
+
+(* Properies on local environment slicing ***********************************)
+
+lemma lpys_ldrop_conf: ∀G. dropable_sn (lpys G).
+/3 width=5 by lpx_sn_deliftable_dropable, cpys_inv_lift1/ qed-.
+
+lemma ldrop_lpys_trans: ∀G. dedropable_sn (lpys G).
+/3 width=9 by lpx_sn_liftable_dedropable, cpys_lift/ qed-.
+
+lemma lpys_ldrop_trans_O1: ∀G. dropable_dx (lpys G).
+/2 width=3 by lpx_sn_dropable/ qed-.
+
+(* Properties on supclosure *************************************************)
+
+lemma fqu_lpys_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
+                      ∀K2. ⦃G2, L2⦄ ⊢ ▶*× K2 →
+                      ∃∃K1,T. ⦃G1, L1⦄ ⊢ ▶*× K1 & ⦃G1, L1⦄ ⊢ T1 ▶*× T & ⦃G1, K1, T⦄ ⊃ ⦃G2, K2, T2⦄.
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+/3 width=5 by fqu_lref_O, fqu_pair_sn, fqu_flat_dx, lpys_pair, ex3_2_intro/
+[ #a #I #G2 #L2 #V2 #T2 #X #H elim (lpys_inv_pair1 … H) -H
+  #K2 #W2 #HLK2 #HVW2 #H destruct
+  /3 width=5 by fqu_fquq, cpys_pair_sn, fqu_bind_dx, ex3_2_intro/
+| #G #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #K2 #HK12
+  elim (ldrop_lpys_trans … HLK1 … HK12) -HK12
+  /3 width=7 by fqu_drop, ex3_2_intro/
+]
+qed-.
+
+lemma fquq_lpys_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+                       ∀K2. ⦃G2, L2⦄ ⊢ ▶*× K2 →
+                       ∃∃K1,T. ⦃G1, L1⦄ ⊢ ▶*× K1 & ⦃G1, L1⦄ ⊢ T1 ▶*× T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄.
+#G1 #G2 #L1 #L2 #T1 #T2 #H #K2 #HLK2 elim (fquq_inv_gen … H) -H
+[ #HT12 elim (fqu_lpys_trans … HT12 … HLK2) /3 width=5 by fqu_fquq, ex3_2_intro/
+| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/
+]
+qed-.
+
+lemma lpys_fqu_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
+                      ∀K1. ⦃G1, K1⦄ ⊢ ▶*× L1 →
+                      ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ▶*× T & ⦃G1, K1, T⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ▶*× L2.
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+/3 width=7 by fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, lpys_pair, ex3_2_intro/
+[ #I #G1 #L1 #V1 #X #H elim (lpys_inv_pair2 … H) -H
+  #K1 #W1 #HKL1 #HWV1 #H destruct elim (lift_total V1 0 1)
+  /4 width=7 by cpys_delta, fqu_drop, ldrop_ldrop, ex3_2_intro/
+| #G #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #L0 #HL01
+  elim (lpys_ldrop_trans_O1 … HL01 … HLK1) -L1
+  /3 width=5 by fqu_drop, ex3_2_intro/
+]
+qed-.
+
+lemma lpys_fquq_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+                       ∀K1. ⦃G1, K1⦄ ⊢ ▶*× L1 →
+                       ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ▶*× T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ▶*× L2.
+#G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #HKL1 elim (fquq_inv_gen … H) -H
+[ #HT12 elim (lpys_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/etc/cpys/lpys_lpys.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/lpys_lpys.etc
new file mode 100644
index 000000000..b9bf06694
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/lpys_lpys.etc
@@ -0,0 +1,39 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/substitution/cpys_cpys.ma".
+
+(* SN EXTENDED MULTIPLE SUBSTITUTION FOR LOCAL ENVIRONMENTS *****************)
+
+(* Main properties **********************************************************)
+
+theorem lpys_trans: ∀G. Transitive … (lpys G).
+/3 width=5 by lpx_sn_trans, cpys_trans_lpys/
+qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma cpys_fwd_shift1_ext: ∀G,L1,L,T1,T. ⦃G, L⦄ ⊢ L1 @@ T1 ▶*× T →
+                           ∃∃L2,T2. ⦃G, L @@ L1⦄ ⊢ ▶*× L @@ L2 & ⦃G, L @@ L1⦄ ⊢ T1 ▶*× T2 &
+                                    T = L2 @@ T2.
+#G #L1 @(lenv_ind_dx … L1) -L1
+[ #L #T1 #T #HT1 @ex3_2_intro
+  [3: // |4,5: // |1,2: skip ] (**) (* auto does not work *)
+| #I #L1 #V1 #IH #L #T1 #T >shift_append_assoc #H <append_assoc
+  elim (cpys_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+  elim (IH … HT12) -IH -HT12 #L2 #T #HL12 #HT1 #H destruct
+  lapply (lpys_trans … HL12 (L.ⓑ{I}V2@@L2) ?) -HL12 /3 width=1 by lpys_append, lpys_pair/ #HL12
+  @(ex3_2_intro … (⋆.ⓑ{I}V2@@L2)) [4: /2 width=3 by trans_eq/ | skip ] <append_assoc // (**) (* explicit constructor *)
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/lsuby.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/lsuby.etc
new file mode 100644
index 000000000..6d5c0072c
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/lsuby.etc
@@ -0,0 +1,75 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/extlrsubeq_2.ma".
+include "basic_2/relocation/ldrop.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR EXTENDED SUBSTITUTION *******************)
+
+inductive lsuby: relation lenv ≝
+| lsuby_atom: ∀L. lsuby L (⋆)
+| lsuby_pair: ∀I1,I2,L1,L2,V. lsuby L1 L2 → lsuby (L1.ⓑ{I1}V) (L2.ⓑ{I2}V)
+.
+
+interpretation
+  "local environment refinement (extended substitution)"
+  'ExtLRSubEq L1 L2 = (lsuby L1 L2).
+
+(* Basic properties *********************************************************)
+
+lemma lsuby_refl: ∀L. L ⊑× L.
+#L elim L -L // /2 width=1/
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lsuby_inv_atom1_aux: ∀L1,L2. L1 ⊑× L2 → L1 = ⋆ → L2 = ⋆.
+#L1 #L2 * -L1 -L2 //
+#I1 #I2 #L1 #L2 #V #_ #H destruct
+qed-.
+
+lemma lsuby_inv_atom1: ∀L2. ⋆ ⊑× L2 → L2 = ⋆.
+/2 width=3 by lsuby_inv_atom1_aux/ qed-.
+
+fact lsuby_inv_pair1_aux: ∀L1,L2. L1 ⊑× L2 → ∀J1,K1,W. L1 = K1.ⓑ{J1}W →
+                          L2 = ⋆ ∨ ∃∃I2,K2. K1 ⊑× K2 & L2 = K2.ⓑ{I2}W.
+#L1 #L2 * -L1 -L2
+[ #L #J1 #K1 #W #H destruct /2 width=1 by or_introl/
+| #I1 #I2 #L1 #L2 #V #HL12 #J1 #K1 #W #H destruct /3 width=4 by ex2_2_intro, or_intror/
+]
+qed-.
+
+lemma lsuby_inv_pair1: ∀I1,K1,L2,W. K1.ⓑ{I1}W ⊑× L2 →
+                       L2 = ⋆ ∨ ∃∃I2,K2. K1 ⊑× K2 & L2 = K2.ⓑ{I2}W.
+/2 width=4 by lsuby_inv_pair1_aux/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lsuby_fwd_length: ∀L1,L2. L1 ⊑× L2 → |L2| ≤ |L1|.
+#L1 #L2 #H elim H -L1 -L2 /2 width=1 by monotonic_le_plus_l/
+qed-.
+
+lemma lsuby_fwd_ldrop2_pair: ∀L1,L2. L1 ⊑× L2 →
+                             ∀I2,K2,W,i. ⇩[0, i] L2 ≡ K2.ⓑ{I2}W →
+                             ∃∃I1,K1. K1 ⊑× K2 & ⇩[0, i] L1 ≡ K1.ⓑ{I1}W.
+#L1 #L2 #H elim H -L1 -L2
+[ #L #J2 #K2 #W #i #H
+  elim (ldrop_inv_atom1 … H) -H #H destruct
+| #I1 #I2 #L1 #L2 #V #HL12 #IHL12 #J2 #K2 #W #i #H
+  elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK2 destruct [ -IHL12 | -HL12 ]
+  [ /3 width=4 by ldrop_pair, ex2_2_intro/
+  | elim (IHL12 … HLK2) -IHL12 -HLK2 * /3 width=4 by ldrop_ldrop_lt, ex2_2_intro/
+  ]
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/lsuby_lsuby.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/lsuby_lsuby.etc
new file mode 100644
index 000000000..590e7d317
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/lsuby_lsuby.etc
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/lsuby.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR EXTENDED SUBSTITUTION *******************)
+
+(* Main properties **********************************************************)
+
+theorem lsuby_trans: Transitive … lsuby.
+#L1 #L #H elim H -L1 -L
+[ #L1 #X #H lapply (lsuby_inv_atom1 … H) -H //
+| #I1 #I #L1 #L #V #_ #IHL1 #X #H elim (lsuby_inv_pair1 … H) -H // *
+  #I2 #L2 #HL2 #H destruct /3 width=1 by lsuby_pair/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/extpsubststaralt_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/extpsubststaralt_6.ma
new file mode 100644
index 000000000..d74b372e8
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/extpsubststaralt_6.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 L ⦄ ⊢ break term 46 T1 break ▶ ▶ * × [ term 46 d , break term 46 e ] break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'ExtPSubstStarAlt $G $L $T1 $d $e $T2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeqalt_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeqalt_3.ma
new file mode 100644
index 000000000..a4d786052
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeqalt_3.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( L1 ⋕ ⋕ break [ term 46 T ] break term 46 L2 )"
+   non associative with precedence 45
+   for @{ 'LazyEqAlt $T $L1 $L2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma
index d6959e253..900bf7d73 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma
@@ -18,9 +18,8 @@ include "basic_2/grammar/cl_shift.ma".
 include "basic_2/relocation/ldrop_append.ma".
 include "basic_2/relocation/lsuby.ma".
 
-(* CONTEXT-SENSITIVE EXTENDED PARALLEL SUBSTITUTION FOR TERMS ***************)
+(* CONTEXT-SENSITIVE EXTENDED ORDINARY SUBSTITUTION FOR TERMS ***************)
 
-(* Note: this substitution is ordinary *)
 (* activate genv *)
 inductive cpy: nat → nat → relation4 genv lenv term term ≝
 | cpy_atom : ∀I,G,L,d,e. cpy d e G L (⓪{I}) (⓪{I})
@@ -34,13 +33,12 @@ inductive cpy: nat → nat → relation4 genv lenv term term ≝
              cpy d e G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
 .
 
-interpretation "context-sensitive extended parallel substritution (term)"
+interpretation "context-sensitive extended ordinary substritution (term)"
    'ExtPSubst G L T1 d e T2 = (cpy d e G L T1 T2).
 
 (* Basic properties *********************************************************)
 
-lemma lsuby_cpy_trans: ∀G,L1,T1,T2,d,e. ⦃G, L1⦄ ⊢ T1 ▶×[d, e] T2 →
-                       ∀L2. L2 ⊑×[d, e] L1 → ⦃G, L2⦄ ⊢ T1 ▶×[d, e] T2.
+lemma lsuby_cpy_trans: ∀G,d,e. lsub_trans … (cpy d e G) (lsuby d e). 
 #G #d #e #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2 -d -e
 [ //
 | #I #G #L1 #K1 #V #W #i #d #e #Hdi #Hide #HLK1 #HVW #L2 #HL12
@@ -150,9 +148,8 @@ lemma cpy_split_down: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶×[d, e] T2 →
 ]
 qed-.
 
-lemma cpy_append: ∀G,K,T1,T2,d,e. ⦃G, K⦄ ⊢ T1 ▶×[d, e] T2 →
-                  ∀L. ⦃G, L @@ K⦄ ⊢ T1 ▶×[d, e] T2.
-#G #K #T1 #T2 #d #e #H elim H -K -T1 -T2 -d -e
+lemma cpy_append: ∀G,d,e. l_appendable_sn … (cpy d e G).
+#G #d #e #K #T1 #T2 #H elim H -K -T1 -T2 -d -e
 /2 width=1 by cpy_atom, cpy_bind, cpy_flat/
 #I #G #K #K0 #V #W #i #d #e #Hdi #Hide #HK0 #HVW #L
 lapply (ldrop_fwd_length_lt2 … HK0) #H
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_cpy.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_cpy.ma
index dd4227b22..f876a53d7 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_cpy.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_cpy.ma
@@ -14,7 +14,7 @@
 
 include "basic_2/relocation/cpy_lift.ma".
 
-(* CONTEXT-SENSITIVE EXTENDED PARALLEL SUBSTITUTION FOR TERMS ***************)
+(* CONTEXT-SENSITIVE EXTENDED ORDINARY SUBSTITUTION FOR TERMS ***************)
 
 (* Main properties **********************************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_lift.ma
index 161b21b01..ebb7c9df2 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_lift.ma
@@ -15,7 +15,7 @@
 include "basic_2/relocation/ldrop_ldrop.ma".
 include "basic_2/relocation/cpy.ma".
 
-(* CONTEXT-SENSITIVE EXTENDED PARALLEL SUBSTITUTION FOR TERMS ***************)
+(* CONTEXT-SENSITIVE EXTENDED ORDINARY SUBSTITUTION FOR TERMS ***************)
 
 (* Relocation properties ****************************************************)
 
@@ -156,11 +156,11 @@ lemma cpy_inv_lift1_be: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 
   elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
   elim (IHV12 … HLK … HWV1) -V1 // #W2 #HW12 #HWV2
   elim (IHU12 … HTU1) -U1
-  [5: @ldrop_skip // |2: skip 
+  [5: /2 width=2 by ldrop_skip/ |2: skip 
   |3: >plus_plus_comm_23 >(plus_plus_comm_23 dt) /2 width=1 by le_S_S/
   |4: /2 width=1 by le_S_S/
-  ] (**) (* 29s without the rewrites *)
-  /3 width=5 by _//3 width=5 by cpy_bind, lift_bind, ex2_intro/
+  ]
+  /3 width=5 by cpy_bind, lift_bind, ex2_intro/
 | #I #G #L #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdtd #Hdedet
   elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
   elim (IHV12 … HLK … HWV1) -V1 //
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq.ma
index 407d414de..b5bef1116 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq.ma
@@ -67,6 +67,10 @@ lemma lleq_ge: ∀L1,L2,T,d1. L1 ⋕[d1, T] L2 → ∀d2. d1 ≤ d2 → L1 ⋕[d
 ]
 qed-.
 
+lemma lleq_bind_O: ∀a,I,L1,L2,V,T. L1 ⋕[0, V] L2 → L1.ⓑ{I}V ⋕[0, T] L2.ⓑ{I}V →
+                   L1 ⋕[0, ⓑ{a,I}V.T] L2.
+/3 width=3 by lleq_ge, lleq_bind/ qed.
+
 (* Basic inversion lemmas ***************************************************)
 
 fact lleq_inv_lref_aux: ∀d,X,L1,L2. L1 ⋕[d, X] L2 → ∀i. X = #i →
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma
index d2aa16144..3c89103c3 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma
@@ -31,10 +31,6 @@ interpretation
   "local environment refinement (extended substitution)"
   'ExtLRSubEq L1 d e L2 = (lsuby d e L1 L2).
 
-definition lsuby_trans: ∀S. predicate (lenv → relation S) ≝ λS,R.
-                        ∀L2,s1,s2. R L2 s1 s2 →
-                        ∀L1,d,e. L1 ⊑×[d, e] L2 → R L1 s1 s2.
-
 (* Basic properties *********************************************************)
 
 lemma lsuby_pair_lt: ∀I1,I2,L1,L2,V,e. L1 ⊑×[0, e-1] L2 → 0 < e →
@@ -62,10 +58,6 @@ lemma lsuby_length: ∀L1,L2. |L2| ≤ |L1| → L1 ⊑×[0, 0] L2.
 ]
 qed.
 
-lemma TC_lsuby_trans: ∀S,R. lsuby_trans S R → lsuby_trans S (λL. (TC … (R L))).
-#S #R #HR #L1 #s1 #s2 #H elim H -s2 /3 width=7 by step, inj/
-qed.
-
 (* Basic inversion lemmas ***************************************************)
 
 fact lsuby_inv_atom1_aux: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 → L1 = ⋆ → L2 = ⋆.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma
index 433718803..91f9f35aa 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma
@@ -12,177 +12,155 @@
 (*                                                                        *)
 (**************************************************************************)
 
-notation "hvbox( L ⊢ break term 46 T1 break ▶ * [ term 46 d , break term 46 e ] break term 46 T2 )"
-   non associative with precedence 45
-   for @{ 'PSubstStar $L $T1 $d $e $T2 }.
+include "basic_2/notation/relations/extpsubststar_6.ma".
+include "basic_2/relocation/cpy.ma".
 
-include "basic_2/substitution/tps.ma".
+(* CONTEXT-SENSITIVE EXTENDED MULTIPLE SUBSTITUTION FOR TERMS ***************)
 
-(* PARTIAL UNFOLD ON TERMS **************************************************)
+definition cpys: nat → nat → relation4 genv lenv term term ≝
+                 λd,e,G. LTC … (cpy d e G).
 
-definition tpss: nat → nat → lenv → relation term ≝
-                 λd,e,L. TC … (tps d e L).
-
-interpretation "partial unfold (term)"
-   'PSubstStar L T1 d e T2 = (tpss d e L T1 T2).
+interpretation "context-sensitive extended multiple substritution (term)"
+   'ExtPSubstStar G L T1 d e T2 = (cpys d e G L T1 T2).
 
 (* Basic eliminators ********************************************************)
 
-lemma tpss_ind: ∀d,e,L,T1. ∀R:predicate term. R T1 →
-                (∀T,T2. L ⊢ T1 ▶* [d, e] T → L ⊢ T ▶ [d, e] T2 → R T → R T2) →
-                ∀T2. L ⊢ T1 ▶* [d, e] T2 → R T2.
-#d #e #L #T1 #R #HT1 #IHT1 #T2 #HT12
+lemma cpys_ind: ∀G,L,T1,d,e. ∀R:predicate term. R T1 →
+                (∀T,T2. ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T → ⦃G, L⦄ ⊢ T ▶×[d, e] T2 → R T → R T2) →
+                ∀T2. ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 → R T2.
+#G #L #T1 #d #e #R #HT1 #IHT1 #T2 #HT12
 @(TC_star_ind … HT1 IHT1 … HT12) //
 qed-.
 
-lemma tpss_ind_dx: ∀d,e,L,T2. ∀R:predicate term. R T2 →
-                   (∀T1,T. L ⊢ T1 ▶ [d, e] T → L ⊢ T ▶* [d, e] T2 → R T → R T1) →
-                   ∀T1. L ⊢ T1 ▶* [d, e] T2 → R T1.
-#d #e #L #T2 #R #HT2 #IHT2 #T1 #HT12
+lemma cpys_ind_dx: ∀G,L,T2,d,e. ∀R:predicate term. R T2 →
+                   (∀T1,T. ⦃G, L⦄ ⊢ T1 ▶×[d, e] T → ⦃G, L⦄ ⊢ T ▶*×[d, e] T2 → R T → R T1) →
+                   ∀T1. ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 → R T1.
+#G #L #T2 #d #e #R #HT2 #IHT2 #T1 #HT12
 @(TC_star_ind_dx … HT2 IHT2 … HT12) //
 qed-.
 
 (* Basic properties *********************************************************)
 
-lemma tps_tpss: ∀L,T1,T2,d,e. L ⊢ T1 ▶ [d, e] T2 → L ⊢ T1 ▶* [d, e] T2.
-/2 width=1/ qed.
-
-lemma tpss_strap1: ∀L,T1,T,T2,d,e.
-                   L ⊢ T1 ▶* [d, e] T → L ⊢ T ▶ [d, e] T2 → L ⊢ T1 ▶* [d, e] T2.
-/2 width=3/ qed.
-
-lemma tpss_strap2: ∀L,T1,T,T2,d,e.
-                   L ⊢ T1 ▶ [d, e] T → L ⊢ T ▶* [d, e] T2 → L ⊢ T1 ▶* [d, e] T2.
-/2 width=3/ qed.
-
-lemma tpss_lsubr_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶* [d, e] T2 →
-                        ∀L2. L2 ⊑ [d, e] L1 → L2 ⊢ T1 ▶* [d, e] T2.
-/3 width=3/ qed.
-
-lemma tpss_refl: ∀d,e,L,T. L ⊢ T ▶* [d, e] T.
-/2 width=1/ qed.
-
-lemma tpss_bind: ∀L,V1,V2,d,e. L ⊢ V1 ▶* [d, e] V2 →
-                 ∀a,I,T1,T2. L. ⓑ{I} V2 ⊢ T1 ▶* [d + 1, e] T2 →
-                 L ⊢ ⓑ{a,I} V1. T1 ▶* [d, e] ⓑ{a,I} V2. T2.
-#L #V1 #V2 #d #e #HV12 elim HV12 -V2
-[ #V2 #HV12 #a #I #T1 #T2 #HT12 elim HT12 -T2
-  [ /3 width=5/
-  | #T #T2 #_ #HT2 #IHT @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
-  ]
-| #V #V2 #_ #HV12 #IHV #a #I #T1 #T2 #HT12
-  lapply (tpss_lsubr_trans … HT12 (L. ⓑ{I} V) ?) -HT12 /2 width=1/ #HT12
-  lapply (IHV a … HT12) -IHV -HT12 #HT12 @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
+lemma cpy_cpys: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶×[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2.
+/2 width=1 by inj/ qed.
+
+lemma cpys_strap1: ∀G,L,T1,T,T2,d,e.
+                   ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T → ⦃G, L⦄ ⊢ T ▶×[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2.
+normalize /2 width=3 by step/ qed-.
+
+lemma cpys_strap2: ∀G,L,T1,T,T2,d,e.
+                   ⦃G, L⦄ ⊢ T1 ▶×[d, e] T → ⦃G, L⦄ ⊢ T ▶*×[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2.
+normalize /2 width=3 by TC_strap/ qed-.
+
+lemma lsuby_cpys_trans: ∀G,d,e. lsub_trans … (cpys d e G) (lsuby d e).
+/3 width=5 by lsuby_cpy_trans, LTC_lsub_trans/
+qed-.
+
+lemma cpys_refl: ∀G,L,d,e. reflexive … (cpys d e G L).
+/2 width=1 by cpy_cpys/ qed.
+
+lemma cpys_bind: ∀G,L,V1,V2,d,e. ⦃G, L⦄ ⊢ V1 ▶*×[d, e] V2 →
+                 ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ▶*×[d+1, e] T2 →
+                 ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*×[d, e] ⓑ{a,I}V2.T2.
+#G #L #V1 #V2 #d #e #HV12 @(cpys_ind … HV12) -V2
+[ #I #T1 #T2 #HT12 @(cpys_ind … HT12) -T2 /3 width=5 by cpys_strap1, cpy_bind/
+| #V #V2 #_ #HV2 #IHV1 #I #T1 #T2 #HT12 #a
+  lapply (lsuby_cpys_trans … HT12 (L.ⓑ{I}V) ?) -HT12
+  /3 width=5 by cpys_strap1, cpy_bind, lsuby_succ/
 ]
 qed.
 
-lemma tpss_flat: ∀L,I,V1,V2,T1,T2,d,e.
-                 L ⊢ V1 ▶* [d, e] V2 → L ⊢ T1 ▶* [d, e] T2 →
-                 L ⊢ ⓕ{I} V1. T1 ▶* [d, e] ⓕ{I} V2. T2.
-#L #I #V1 #V2 #T1 #T2 #d #e #HV12 elim HV12 -V2
-[ #V2 #HV12 #HT12 elim HT12 -T2
-  [ /3 width=1/
-  | #T #T2 #_ #HT2 #IHT @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
-  ]
-| #V #V2 #_ #HV12 #IHV #HT12
-  lapply (IHV … HT12) -IHV -HT12 #HT12 @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
-]
+lemma cpys_flat: ∀G,L,V1,V2,d,e. ⦃G, L⦄ ⊢ V1 ▶*×[d, e] V2 →
+                 ∀T1,T2. ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 →
+                 ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ▶*×[d, e] ⓕ{I}V2.T2.
+#G #L #V1 #V2 #d #e #HV12 @(cpys_ind … HV12) -V2
+[ #T1 #T2 #HT12 @(cpys_ind … HT12) -T2 /3 width=5 by cpys_strap1, cpy_flat/
+| /3 width=5 by cpys_strap1, cpy_flat/
 qed.
 
-lemma tpss_weak: ∀L,T1,T2,d1,e1. L ⊢ T1 ▶* [d1, e1] T2 →
+lemma cpys_weak: ∀G,L,T1,T2,d1,e1. ⦃G, L⦄ ⊢ T1 ▶*×[d1, e1] T2 →
                  ∀d2,e2. d2 ≤ d1 → d1 + e1 ≤ d2 + e2 →
-                 L ⊢ T1 ▶* [d2, e2] T2.
-#L #T1 #T2 #d1 #e1 #H #d1 #d2 #Hd21 #Hde12 @(tpss_ind … H) -T2
-[ //
-| #T #T2 #_ #HT12 #IHT
-  lapply (tps_weak … HT12 … Hd21 Hde12) -HT12 -Hd21 -Hde12 /2 width=3/
-]
-qed.
+                 ⦃G, L⦄ ⊢ T1 ▶*×[d2, e2] T2.
+#G #L #T1 #T2 #d1 #e1 #H #d1 #d2 #Hd21 #Hde12 @(cpys_ind … H) -T2
+/3 width=7 by cpys_strap1, cpy_weak/
+qed-.
 
-lemma tpss_weak_top: ∀L,T1,T2,d,e.
-                     L ⊢ T1 ▶* [d, e] T2 → L ⊢ T1 ▶* [d, |L| - d] T2.
-#L #T1 #T2 #d #e #H @(tpss_ind … H) -T2
-[ //
-| #T #T2 #_ #HT12 #IHT
-  lapply (tps_weak_top … HT12) -HT12 /2 width=3/
-]
-qed.
+lemma cpys_weak_top: ∀G,L,T1,T2,d,e.
+                     ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶*×[d, |L| - d] T2.
+#G #L #T1 #T2 #d #e #H @(cpys_ind … H) -T2
+/3 width=4 by cpys_strap1, cpy_weak_top/
+qed-.
 
-lemma tpss_weak_full: ∀L,T1,T2,d,e.
-                      L ⊢ T1 ▶* [d, e] T2 → L ⊢ T1 ▶* [0, |L|] T2.
-#L #T1 #T2 #d #e #HT12
-lapply (tpss_weak … HT12 0 (d + e) ? ?) -HT12 // #HT12
-lapply (tpss_weak_top … HT12) //
-qed.
+lemma cpys_weak_full: ∀G,L,T1,T2,d,e.
+                      ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶*×[0, |L|] T2.
+#G #L #T1 #T2 #d #e #H @(cpys_ind … H) -T2
+/3 width=5 by cpys_strap1, cpy_weak_full/
+qed-.
 
-lemma tpss_append: ∀K,T1,T2,d,e. K ⊢ T1 ▶* [d, e] T2 →
-                   ∀L. L @@ K ⊢ T1 ▶* [d, e] T2.
-#K #T1 #T2 #d #e #H @(tpss_ind … H) -T2 // /3 width=3/
-qed.
+lemma cpys_append: ∀G,d,e. l_appendable_sn … (cpys d e G).
+#G #d #e #K #T1 #T2 #H @(cpys_ind … H) -T2
+/3 width=3 by cpys_strap1, cpy_append/
+qed-.
 
 (* Basic inversion lemmas ***************************************************)
 
-(* Note: this can be derived from tpss_inv_atom1 *)
-lemma tpss_inv_sort1: ∀L,T2,k,d,e. L ⊢ ⋆k ▶* [d, e] T2 → T2 = ⋆k.
-#L #T2 #k #d #e #H @(tpss_ind … H) -T2
-[ //
-| #T #T2 #_ #HT2 #IHT destruct
-  >(tps_inv_sort1 … HT2) -HT2 //
-]
+(* Note: this can be derived from cpys_inv_atom1 *)
+lemma cpys_inv_sort1: ∀G,L,T2,k,d,e. ⦃G, L⦄ ⊢ ⋆k ▶*×[d, e] T2 → T2 = ⋆k.
+#G #L #T2 #k #d #e #H @(cpys_ind … H) -T2 //
+#T #T2 #_ #HT2 #IHT1 destruct
+>(cpy_inv_sort1 … HT2) -HT2 //
 qed-.
 
-(* Note: this can be derived from tpss_inv_atom1 *)
-lemma tpss_inv_gref1: ∀L,T2,p,d,e. L ⊢ §p ▶* [d, e] T2 → T2 = §p.
-#L #T2 #p #d #e #H @(tpss_ind … H) -T2
-[ //
-| #T #T2 #_ #HT2 #IHT destruct
-  >(tps_inv_gref1 … HT2) -HT2 //
-]
+(* Note: this can be derived from cpys_inv_atom1 *)
+lemma cpys_inv_gref1: ∀G,L,T2,p,d,e. ⦃G, L⦄ ⊢ §p ▶*×[d, e] T2 → T2 = §p.
+#G #L #T2 #p #d #e #H @(cpys_ind … H) -T2 //
+#T #T2 #_ #HT2 #IHT1 destruct
+>(cpy_inv_gref1 … HT2) -HT2 //
 qed-.
 
-lemma tpss_inv_bind1: ∀d,e,L,a,I,V1,T1,U2. L ⊢ ⓑ{a,I} V1. T1 ▶* [d, e] U2 →
-                      ∃∃V2,T2. L ⊢ V1 ▶* [d, e] V2 &
-                               L. ⓑ{I} V2 ⊢ T1 ▶* [d + 1, e] T2 &
-                               U2 = ⓑ{a,I} V2. T2.
-#d #e #L #a #I #V1 #T1 #U2 #H @(tpss_ind … H) -U2
-[ /2 width=5/
+lemma cpys_inv_bind1: ∀a,I,G,L,V1,T1,U2,d,e. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*×[d, e] U2 →
+                      ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*×[d, e] V2 &
+                               ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ▶*×[d+1, e] T2 &
+                               U2 = ⓑ{a,I}V2.T2.
+#a #I #G #L #V1 #T1 #U2 #d #e #H @(cpys_ind … H) -U2
+[ /2 width=5 by ex3_2_intro/
 | #U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct
-  elim (tps_inv_bind1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H
-  lapply (tpss_lsubr_trans … HT1 (L. ⓑ{I} V2) ?) -HT1 /2 width=1/ /3 width=5/
+  elim (cpy_inv_bind1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H
+  lapply (lsuby_cpys_trans … HT1 (L.ⓑ{I}V2) ?) -HT1
+  /3 width=5 by cpys_strap1, lsuby_succ, ex3_2_intro/
 ]
 qed-.
 
-lemma tpss_inv_flat1: ∀d,e,L,I,V1,T1,U2. L ⊢ ⓕ{I} V1. T1 ▶* [d, e] U2 →
-                      ∃∃V2,T2. L ⊢ V1 ▶* [d, e] V2 & L ⊢ T1 ▶* [d, e] T2 &
-                               U2 =  ⓕ{I} V2. T2.
-#d #e #L #I #V1 #T1 #U2 #H @(tpss_ind … H) -U2
-[ /2 width=5/
+lemma cpys_inv_flat1: ∀I,G,L,V1,T1,U2,d,e. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ▶*×[d, e] U2 →
+                      ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*×[d, e] V2 & ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 &
+                               U2 = ⓕ{I}V2.T2.
+#I #G #L #V1 #T1 #U2 #d #e #H @(cpys_ind … H) -U2
+[ /2 width=5 by ex3_2_intro/
 | #U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct
-  elim (tps_inv_flat1 … HU2) -HU2 /3 width=5/
+  elim (cpy_inv_flat1 … HU2) -HU2
+  /3 width=5 by cpys_strap1, ex3_2_intro/
 ]
 qed-.
 
-lemma tpss_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 ▶* [d, 0] T2 → T1 = T2.
-#L #T1 #T2 #d #H @(tpss_ind … H) -T2
-[ //
-| #T #T2 #_ #HT2 #IHT <(tps_inv_refl_O2 … HT2) -HT2 //
-]
+lemma cpys_inv_refl_O2: ∀G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 ▶*×[d, 0] T2 → T1 = T2.
+#G #L #T1 #T2 #d #H @(cpys_ind … H) -T2 //
+#T #T2 #_ #HT2 #IHT1 <(cpy_inv_refl_O2 … HT2) -HT2 //
 qed-.
 
 (* Basic forward lemmas *****************************************************)
 
-lemma tpss_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e] T2 → ♯{T1} ≤ ♯{T2}.
-#L #T1 #T2 #d #e #H @(tpss_ind … H) -T2 //
-#T #T2 #_ #HT2 #IHT1
-lapply (tps_fwd_tw … HT2) -HT2 #HT2
-@(transitive_le … IHT1) //
+lemma cpys_fwd_tw: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 → ♯{T1} ≤ ♯{T2}.
+#G #L #T1 #T2 #d #e #H @(cpys_ind … H) -T2 //
+#T #T2 #_ #HT2 #IHT1 lapply (cpy_fwd_tw … HT2) -HT2
+/2 width=3 by transitive_le/
 qed-.
 
-lemma tpss_fwd_shift1: ∀L,L1,T1,T,d,e. L ⊢ L1 @@ T1 ▶*[d, e] T →
+lemma cpys_fwd_shift1: ∀G,L,L1,T1,T,d,e. ⦃G, L⦄ ⊢ L1 @@ T1 ▶*×[d, e] T →
                        ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2.
-#L #L1 #T1 #T #d #e #H @(tpss_ind … H) -T
-[ /2 width=4/
-| #T #X #_ #H0 * #L0 #T0 #HL10 #H destruct
-  elim (tps_fwd_shift1 … H0) -H0 #L2 #T2 #HL02 #H destruct /2 width=4/
+#G #L #L1 #T1 #T #d #e #H @(cpys_ind … H) -T
+[ /2 width=4 by ex2_2_intro/
+| #T #X #_ #HX * #L0 #T0 #HL10 #H destruct
+  elim (cpy_fwd_shift1 … HX) -HX #L2 #T2 #HL02 #H destruct
+  /2 width=4 by ex2_2_intro/
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma
new file mode 100644
index 000000000..cf0b10e76
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma
@@ -0,0 +1,102 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/extpsubststaralt_6.ma".
+include "basic_2/substitution/cpys_lift.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED MULTIPLE SUBSTITUTION FOR TERMS ***************)
+
+(* alternative definition of cpys *)
+inductive cpysa: nat → nat → relation4 genv lenv term term ≝
+| cpysa_atom : ∀I,G,L,d,e. cpysa d e G L (⓪{I}) (⓪{I})
+| cpysa_subst: ∀I,G,L,K,V1,V2,W2,i,d,e. d ≤ i → i < d + e →
+               ⇩[0, i] L ≡ K.ⓑ{I}V1 → cpysa 0 (d+e-i-1) G K V1 V2 →
+               ⇧[0, i+1] V2 ≡ W2 → cpysa d e G L (#i) W2
+| cpysa_bind : ∀a,I,G,L,V1,V2,T1,T2,d,e.
+               cpysa d e G L V1 V2 → cpysa (d + 1) e G (L.ⓑ{I}V2) T1 T2 →
+               cpysa d e G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
+| cpysa_flat : ∀I,G,L,V1,V2,T1,T2,d,e.
+               cpysa d e G L V1 V2 → cpysa d e G L T1 T2 →
+               cpysa d e G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
+.
+
+interpretation
+   "context-sensitive extended multiple substritution (term) alternative"
+   'ExtPSubstStarAlt G L T1 d e T2 = (cpysa d e G L T1 T2).
+
+(* Basic properties *********************************************************)
+
+lemma lsuby_cpysa_trans: ∀G,d,e. lsub_trans … (cpysa d e G) (lsuby d e).
+#G #d #e #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2 -d -e
+[ //
+| #I #G #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
+  elim (lsuby_fwd_ldrop2_be … HL12 … HLK1) -HL12 -HLK1 /3 width=7 by cpysa_subst/
+| /4 width=1 by lsuby_succ, cpysa_bind/
+| /3 width=1 by cpysa_flat/
+]
+qed-.
+
+lemma cpysa_refl: ∀G,T,L,d,e. ⦃G, L⦄ ⊢ T ▶▶*×[d, e] T.
+#G #T elim T -T //
+#I elim I -I /2 width=1 by cpysa_bind, cpysa_flat/
+qed.
+
+lemma cpysa_cpy_trans: ∀G,L,T1,T,d,e. ⦃G, L⦄ ⊢ T1 ▶▶*×[d, e] T →
+                       ∀T2. ⦃G, L⦄ ⊢ T ▶×[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶▶*×[d, e] T2.
+#G #L #T1 #T #d #e #H elim H -G -L -T1 -T -d -e
+[ #I #G #L #d #e #X #H
+  elim (cpy_inv_atom1 … H) -H // * /2 width=7 by cpysa_subst/
+| #I #G #L #K #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK #_ #HVW2 #IHV12 #T2 #H
+  lapply (ldrop_fwd_ldrop2 … HLK) #H0LK
+  lapply (cpy_weak … H 0 (d+e) ? ?) -H // #H
+  elim (cpy_inv_lift1_be … H … H0LK … HVW2) -H -H0LK -HVW2 /3 width=7 by cpysa_subst/
+| #a #I #G #L #V1 #V #T1 #T #d #e #_ #_ #IHV1 #IHT1 #X #H
+  elim (cpy_inv_bind1 … H) -H #V2 #T2 #HV2 #HT2 #H destruct
+  lapply (lsuby_cpy_trans … HT2 (L.ⓑ{I}V) ?) -HT2 /2 width=1 by lsuby_succ/ #HT2
+  lapply (IHV1 … HV2) -IHV1 -HV2 #HV12
+  lapply (IHT1 … HT2) -IHT1 -HT2 #HT12
+  lapply (lsuby_cpysa_trans … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1 by lsuby_succ, cpysa_bind/
+| #I #G #L #V1 #V #T1 #T #d #e #_ #_ #IHV1 #IHT1 #X #H
+  elim (cpy_inv_flat1 … H) -H #V2 #T2 #HV2 #HT2 #H destruct /3 width=1 by cpysa_flat/
+]
+qed-.
+
+lemma cpys_cpysa: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶▶*×[d, e] T2.
+/3 width=8 by cpysa_cpy_trans, cpys_ind/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma cpysa_cpys: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶▶*×[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2.
+#G #L #T1 #T2 #d #e #H elim H -G -L -T1 -T2 -d -e
+/2 width=7 by cpys_subst, cpys_flat, cpys_bind, cpy_cpys/
+qed-.
+
+lemma cpys_ind_alt: ∀R:nat→nat→relation4 genv lenv term term.
+                    (∀I,G,L,d,e. R d e G L (⓪{I}) (⓪{I})) →
+                    (∀I,G,L,K,V1,V2,W2,i,d,e. d ≤ i → i < d + e →
+                     ⇩[O, i] L ≡ K.ⓑ{I}V1 → ⦃G, K⦄ ⊢ V1 ▶*×[O, d+e-i-1] V2 →
+                     ⇧[O, i + 1] V2 ≡ W2 → R O (d+e-i-1) G K V1 V2 → R d e G L (#i) W2
+                    ) →
+                    (∀a,I,G,L,V1,V2,T1,T2,d,e. ⦃G, L⦄ ⊢ V1 ▶*×[d, e] V2 →
+                     ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ▶*×[d + 1, e] T2 → R d e G L V1 V2 →
+                     R (d+1) e G (L.ⓑ{I}V2) T1 T2 → R d e G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
+                    ) →
+                    (∀I,G,L,V1,V2,T1,T2,d,e. ⦃G, L⦄ ⊢ V1 ▶*×[d, e] V2 →
+                     ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 → R d e G L V1 V2 →
+                     R d e G L T1 T2 → R d e G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
+                    ) →
+                    ∀d,e,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 → R d e G L T1 T2.
+#R #H1 #H2 #H3 #H4 #d #e #G #L #T1 #T2 #H elim (cpys_cpysa … H) -G -L -T1 -T2 -d -e
+/3 width=8 by cpysa_cpys/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cpys.ma
new file mode 100644
index 000000000..f84916b9b
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cpys.ma
@@ -0,0 +1,94 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/cpy_cpy.ma".
+include "basic_2/substitution/cpys_lift.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED MULTIPLE SUBSTITUTION FOR TERMS ***************)
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma cpys_inv_SO2: ∀G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 ▶*×[d, 1] T2 → ⦃G, L⦄ ⊢ T1 ▶×[d, 1] T2.
+#G #L #T1 #T2 #d #H @(cpys_ind … H) -T2 /2 width=3 by cpy_trans_ge/
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma cpys_strip_eq: ∀G,L,T0,T1,d1,e1. ⦃G, L⦄ ⊢ T0 ▶*×[d1, e1] T1 →
+                     ∀T2,d2,e2. ⦃G, L⦄ ⊢ T0 ▶×[d2, e2] T2 →
+                     ∃∃T. ⦃G, L⦄ ⊢ T1 ▶×[d2, e2] T & ⦃G, L⦄ ⊢ T2 ▶*×[d1, e1] T.
+normalize /3 width=3 by cpy_conf_eq, TC_strip1/ qed-.
+
+lemma cpys_strip_neq: ∀G,L1,T0,T1,d1,e1. ⦃G, L1⦄ ⊢ T0 ▶*×[d1, e1] T1 →
+                      ∀L2,T2,d2,e2. ⦃G, L2⦄ ⊢ T0 ▶×[d2, e2] T2 →
+                      (d1 + e1 ≤ d2 ∨ d2 + e2 ≤ d1) →
+                      ∃∃T. ⦃G, L2⦄ ⊢ T1 ▶×[d2, e2] T & ⦃G, L1⦄ ⊢ T2 ▶*×[d1, e1] T.
+normalize /3 width=3 by cpy_conf_neq, TC_strip1/ qed-.
+
+lemma cpys_strap1_down: ∀G,L,T1,T0,d1,e1. ⦃G, L⦄ ⊢ T1 ▶*×[d1, e1] T0 →
+                        ∀T2,d2,e2. ⦃G, L⦄ ⊢ T0 ▶×[d2, e2] T2 → d2 + e2 ≤ d1 →
+                        ∃∃T. ⦃G, L⦄ ⊢ T1 ▶×[d2, e2] T & ⦃G, L⦄ ⊢ T ▶*×[d1, e1] T2.
+normalize /3 width=3 by cpy_trans_down, TC_strap1/ qed.
+
+lemma cpys_strap2_down: ∀G,L,T1,T0,d1,e1. ⦃G, L⦄ ⊢ T1 ▶×[d1, e1] T0 →
+                        ∀T2,d2,e2. ⦃G, L⦄ ⊢ T0 ▶*×[d2, e2] T2 → d2 + e2 ≤ d1 →
+                        ∃∃T. ⦃G, L⦄ ⊢ T1 ▶*×[d2, e2] T & ⦃G, L⦄ ⊢ T ▶×[d1, e1] T2.
+normalize /3 width=3 by cpy_trans_down, TC_strap2/ qed-.
+
+lemma cpys_split_up: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 →
+                     ∀i. d ≤ i → i ≤ d + e →
+                     ∃∃T. ⦃G, L⦄ ⊢ T1 ▶*×[d, i - d] T & ⦃G, L⦄ ⊢ T ▶*×[i, d + e - i] T2.
+#G #L #T1 #T2 #d #e #H #i #Hdi #Hide @(cpys_ind … H) -T2
+[ /2 width=3 by ex2_intro/
+| #T #T2 #_ #HT12 * #T3 #HT13 #HT3
+  elim (cpy_split_up … HT12 … Hdi Hide) -HT12 -Hide #T0 #HT0 #HT02
+  elim (cpys_strap1_down … HT3 … HT0 ?) -T /3 width=5 by cpys_strap1, ex2_intro/
+  >commutative_plus /2 width=1 by le_minus_to_plus_r/
+]
+qed-.
+
+lemma cpys_inv_lift1_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 →
+                         ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
+                         d ≤ dt → dt ≤ d + e → d + e ≤ dt + et →
+                         ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[d, dt + et - (d + e)] T2 &
+                               ⇧[d, e] T2 ≡ U2.
+#G #L #U1 #U2 #dt #et #HU12 #K #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet
+elim (cpys_split_up … HU12 (d + e)) -HU12 // -Hdedet #U #HU1 #HU2
+lapply (cpys_weak … HU1 d e ? ?) -HU1 // [ >commutative_plus /2 width=1 by le_minus_to_plus_r/ ] -Hddt -Hdtde #HU1
+lapply (cpys_inv_lift1_eq … HU1 … HTU1) -HU1 #HU1 destruct
+elim (cpys_inv_lift1_ge … HU2 … HLK … HTU1) -HU2 -HLK -HTU1 // <minus_plus_m_m /2 width=3 by ex2_intro/
+qed-.
+
+(* Main properties **********************************************************)
+
+theorem cpys_conf_eq: ∀G,L,T0,T1,d1,e1. ⦃G, L⦄ ⊢ T0 ▶*×[d1, e1] T1 →
+                      ∀T2,d2,e2. ⦃G, L⦄ ⊢ T0 ▶*×[d2, e2] T2 →
+                      ∃∃T. ⦃G, L⦄ ⊢ T1 ▶*×[d2, e2] T & ⦃G, L⦄ ⊢ T2 ▶*×[d1, e1] T.
+normalize /3 width=3 by cpy_conf_eq, TC_confluent2/ qed-.
+
+theorem cpys_conf_neq: ∀G,L1,T0,T1,d1,e1. ⦃G, L1⦄ ⊢ T0 ▶*×[d1, e1] T1 →
+                       ∀L2,T2,d2,e2. ⦃G, L2⦄ ⊢ T0 ▶*×[d2, e2] T2 →
+                       (d1 + e1 ≤ d2 ∨ d2 + e2 ≤ d1) →
+                       ∃∃T. ⦃G, L2⦄ ⊢ T1 ▶*×[d2, e2] T & ⦃G, L1⦄ ⊢ T2 ▶*×[d1, e1] T.
+normalize /3 width=3 by cpy_conf_neq, TC_confluent2/ qed-.
+
+theorem cpys_trans_eq: ∀G,L,T1,T,T2,d,e.
+                       ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T → ⦃G, L⦄ ⊢ T ▶*×[d, e] T2 →
+                       ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2.
+normalize /2 width=3 by trans_TC/ qed-.
+
+theorem cpys_trans_down: ∀G,L,T1,T0,d1,e1. ⦃G, L⦄ ⊢ T1 ▶*×[d1, e1] T0 →
+                         ∀T2,d2,e2. ⦃G, L⦄ ⊢ T0 ▶*×[d2, e2] T2 → d2 + e2 ≤ d1 →
+                         ∃∃T. ⦃G, L⦄ ⊢ T1 ▶*×[d2, e2] T & ⦃G, L⦄ ⊢ T ▶*×[d1, e1] T2.
+normalize /3 width=3 by cpy_trans_down, TC_transitive2/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma
new file mode 100644
index 000000000..631ab202d
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma
@@ -0,0 +1,183 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/cpy_lift.ma".
+include "basic_2/substitution/cpys.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED MULTIPLE SUBSTITUTION FOR TERMS ***************)
+
+(* Advanced properties ******************************************************)
+
+lemma cpys_subst: ∀I,G,L,K,V,U1,i,d,e.
+                  d ≤ i → i < d + e →
+                  ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ▶*×[0, d+e-i-1] U1 →
+                  ∀U2. ⇧[0, i + 1] U1 ≡ U2 → ⦃G, L⦄ ⊢ #i ▶*×[d, e] U2.
+#I #G #L #K #V #U1 #i #d #e #Hdi #Hide #HLK #H @(cpys_ind … H) -U1
+[ /3 width=5 by cpy_cpys, cpy_subst/
+| #U #U1 #_ #HU1 #IHU #U2 #HU12
+  elim (lift_total U 0 (i+1)) #U0 #HU0
+  lapply (IHU … HU0) -IHU #H
+  lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
+  lapply (cpy_lift_ge … HU1 … HLK HU0 HU12 ?) -HU1 -HLK -HU0 -HU12 // normalize #HU02
+  lapply (cpy_weak … HU02 d e ? ?) -HU02 [2,3: /2 width=3 by cpys_strap1, le_S/ ]
+  >minus_plus >commutative_plus /2 width=1 by le_minus_to_plus_r/
+]
+qed.
+
+(* Advanced inverion lemmas *************************************************)
+
+lemma cpys_inv_atom1: ∀G,L,T2,I,d,e. ⦃G, L⦄ ⊢ ⓪{I} ▶*×[d, e] T2 →
+                      T2 = ⓪{I} ∨
+                      ∃∃J,K,V1,V2,i. d ≤ i & i < d + e &
+                                    ⇩[O, i] L ≡ K.ⓑ{J}V1 &
+                                     ⦃G, K⦄ ⊢ V1 ▶*×[0, d+e-i-1] V2 &
+                                     ⇧[O, i + 1] V2 ≡ T2 &
+                                     I = LRef i.
+#G #L #T2 #I #d #e #H @(cpys_ind … H) -T2
+[ /2 width=1 by or_introl/
+| #T #T2 #_ #HT2 *
+  [ #H destruct
+    elim (cpy_inv_atom1 … HT2) -HT2 [ /2 width=1 by or_introl/ | * /3 width=11 by ex6_5_intro, or_intror/ ]
+  | * #J #K #V1 #V #i #Hdi #Hide #HLK #HV1 #HVT #HI
+    lapply (ldrop_fwd_ldrop2 … HLK) #H
+    elim (cpy_inv_lift1_ge_up … HT2 … H … HVT) normalize -HT2 -H -HVT [2,3,4: /2 width=1 by le_S/ ]
+    <minus_plus /4 width=11 by cpys_strap1, ex6_5_intro, or_intror/
+  ]
+]
+qed-.
+
+lemma cpys_inv_lref1: ∀G,L,T2,i,d,e. ⦃G, L⦄ ⊢ #i ▶*×[d, e] T2 →
+                      T2 = #i ∨
+                      ∃∃I,K,V1,V2. d ≤ i & i < d + e &
+                                   ⇩[O, i] L ≡ K.ⓑ{I}V1 &
+                                   ⦃G, K⦄ ⊢ V1 ▶*×[0, d + e - i - 1] V2 &
+                                   ⇧[O, i + 1] V2 ≡ T2.
+#G #L #T2 #i #d #e #H elim (cpys_inv_atom1 … H) -H /2 width=1 by or_introl/
+* #I #K #V1 #V2 #j #Hdj #Hjde #HLK #HV12 #HVT2 #H destruct /3 width=7 by ex5_4_intro, or_intror/
+qed-.
+
+(* Relocation properties ****************************************************)
+
+lemma cpys_lift_le: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*×[dt, et] T2 →
+                    ∀L,U1,d,e. dt + et ≤ d → ⇩[d, e] L ≡ K →
+                    ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 →
+                    ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2.
+#G #K #T1 #T2 #dt #et #H #L #U1 #d #e #Hdetd #HLK #HTU1 @(cpys_ind … H) -T2
+[ #U2 #H >(lift_mono … HTU1 … H) -H //
+| -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
+  elim (lift_total T d e) #U #HTU
+  lapply (IHT … HTU) -IHT #HU1
+  lapply (cpy_lift_le … HT2 … HLK HTU HTU2 ?) -HT2 -HLK -HTU -HTU2 /2 width=3 by cpys_strap1/
+]
+qed-.
+
+lemma cpys_lift_be: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*×[dt, et] T2 →
+                    ∀L,U1,d,e. dt ≤ d → d ≤ dt + et →
+                    ⇩[d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 →
+                    ∀U2. ⇧[d, e] T2 ≡ U2 → ⦃G, L⦄ ⊢ U1 ▶*×[dt, et + e] U2.
+#G #K #T1 #T2 #dt #et #H #L #U1 #d #e #Hdtd #Hddet #HLK #HTU1 @(cpys_ind … H) -T2
+[ #U2 #H >(lift_mono … HTU1 … H) -H //
+| -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
+  elim (lift_total T d e) #U #HTU
+  lapply (IHT … HTU) -IHT #HU1
+  lapply (cpy_lift_be … HT2 … HLK HTU HTU2 ? ?) -HT2 -HLK -HTU -HTU2 /2 width=3 by cpys_strap1/
+]
+qed-.
+
+lemma cpys_lift_ge: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*×[dt, et] T2 →
+                    ∀L,U1,d,e. d ≤ dt → ⇩[d, e] L ≡ K →
+                    ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 →
+                    ⦃G, L⦄ ⊢ U1 ▶*×[dt + e, et] U2.
+#G #K #T1 #T2 #dt #et #H #L #U1 #d #e #Hddt #HLK #HTU1 @(cpys_ind … H) -T2
+[ #U2 #H >(lift_mono … HTU1 … H) -H //
+| -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
+  elim (lift_total T d e) #U #HTU
+  lapply (IHT … HTU) -IHT #HU1
+  lapply (cpy_lift_ge … HT2 … HLK HTU HTU2 ?) -HT2 -HLK -HTU -HTU2 /2 width=3 by cpys_strap1/
+]
+qed-.
+
+lemma cpys_inv_lift1_le: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 →
+                         ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
+                         dt + et ≤ d →
+                         ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[dt, et] T2 & ⇧[d, e] T2 ≡ U2.
+#G #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdetd @(cpys_ind … H) -U2
+[ /2 width=3 by ex2_intro/
+| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
+  elim (cpy_inv_lift1_le … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
+]
+qed-.
+
+lemma cpys_inv_lift1_be: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 →
+                         ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
+                         dt ≤ d → d + e ≤ dt + et →
+                         ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[dt, et - e] T2 & ⇧[d, e] T2 ≡ U2.
+#G #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdedet @(cpys_ind … H) -U2
+[ /2 width=3 by ex2_intro/
+| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
+  elim (cpy_inv_lift1_be … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
+]
+qed-.
+
+lemma cpys_inv_lift1_ge: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 →
+                         ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
+                         d + e ≤ dt →
+                         ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[dt - e, et] T2 & ⇧[d, e] T2 ≡ U2.
+#G #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdedt @(cpys_ind … H) -U2
+[ /2 width=3 by ex2_intro/
+| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
+  elim (cpy_inv_lift1_ge … HU2 … HLK … HTU ?) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
+]
+qed-.
+
+lemma cpys_inv_lift1_eq: ∀G,L,U1,U2,d,e.
+                         ⦃G, L⦄ ⊢ U1 ▶*×[d, e] U2 → ∀T1. ⇧[d, e] T1 ≡ U1 → U1 = U2.
+#G #L #U1 #U2 #d #e #H #T1 #HTU1 @(cpys_ind … H) -U2 //
+#U #U2 #_ #HU2 #IHU destruct
+<(cpy_inv_lift1_eq … HU2 … HTU1) -HU2 -HTU1 //
+qed-.
+
+lemma cpys_inv_lift1_ge_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 →
+                            ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
+                            d ≤ dt → dt ≤ d + e → d + e ≤ dt + et →
+                            ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[d, dt + et - (d + e)] T2 &
+                                 ⇧[d, e] T2 ≡ U2.
+#G #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet @(cpys_ind … H) -U2
+[ /2 width=3 by ex2_intro/
+| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
+  elim (cpy_inv_lift1_ge_up … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
+]
+qed-.
+
+lemma cpys_inv_lift1_be_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 →
+                            ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
+                            dt ≤ d → dt + et ≤ d + e →
+                            ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[dt, d - dt] T2 & ⇧[d, e] T2 ≡ U2.
+#G #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdetde @(cpys_ind … H) -U2
+[ /2 width=3 by ex2_intro/
+| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
+  elim (cpy_inv_lift1_be_up … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
+]
+qed-.
+
+lemma cpys_inv_lift1_le_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 →
+                            ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
+                            dt ≤ d → d ≤ dt + et → dt + et ≤ d + e →
+                            ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[dt, d - dt] T2 & ⇧[d, e] T2 ≡ U2.
+#G #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hddet #Hdetde @(cpys_ind … H) -U2
+[ /2 width=3 by ex2_intro/
+| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
+  elim (cpy_inv_lift1_le_up … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
+]
+qed-.
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 5c4006b1c..f4fa07485 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
@@ -208,6 +208,10 @@ table {
    ]
    class "yellow"
    [ { "substitution" * } {
+        [ { "contxt-sensitive extended multiple substitution" * } {
+             [ "cpys ( ⦃?,?⦄ ⊢ ? ▶*×[?,?] ? )" "cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*×[?,?] ? )" "cpys_lift" + "cpys_cpys" * ]
+          }
+        ]        
         [ { "iterated structural successor for closures" * } {
              [ "fqus ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ )" "fqus_alt" + "fqus_lleq" + "fqus_fqus" * ]
              [ "fqup ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ )" "fqup_lleq" + "fqup_fqup" * ]
@@ -230,16 +234,11 @@ table {
    ]
    class "orange"
    [ { "relocation" * } {
-        [ { "structural successor for closures" * } {
-             [ "fquq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ )" "fquq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ )" "fquq_lleq" * ]
-             [ "fqu ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ )" "fqu_lleq" * ]
-          }
-        ]
         [ { "lazy equivalence for local environments" * } {
              [ "lleq ( ? ⋕[?,?] ? )" "lleq_lleq" * ]
           }
         ]
-        [ { "contxt-sensitive extended substitution" * } {
+        [ { "contxt-sensitive extended ordinary substitution" * } {
              [ "cpy ( ⦃?,?⦄ ⊢ ? ▶×[?,?] ? )" "cpy_lift" + "cpy_cpy" * ]
           }
         ]        
@@ -251,6 +250,11 @@ table {
              [ "lsubr ( ? ⊑ ? )" "lsubr_lsubr" * ]
           }
         ]
+        [ { "structural successor for closures" * } {
+             [ "fquq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ )" "fquq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ )" "fquq_lleq" * ]
+             [ "fqu ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ )" "fqu_lleq" * ]
+          }
+        ]
         [ { "global env. slicing" * } {
              [ "gdrop ( ⇩[?] ? ≡ ? )" "gdrop_gdrop" * ]
           }
diff --git a/matita/matita/contribs/lambdadelta/etc2ma.sh b/matita/matita/contribs/lambdadelta/etc2ma.sh
new file mode 100644
index 000000000..c2d6481ef
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/etc2ma.sh
@@ -0,0 +1 @@
+for FILE in `find $1 -name "*.etc"`; do svn mv $FILE ${FILE/%.etc/.ma} ; done
diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma
index e5b788766..8cfdf349e 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma
@@ -154,7 +154,7 @@ lemma NF_to_SN_sn: ∀A,R,S,a. NF_sn A R S a → SN_sn A R S a.
 elim HSa12 -HSa12 /2 width=1/
 qed.
 
-lemma TC_lsub_trans: ∀A,B,R,S. lsub_trans A B R S → lsub_trans A B (LTC … R) S.
+lemma LTC_lsub_trans: ∀A,B,R,S. lsub_trans A B R S → lsub_trans A B (LTC … R) S.
 #A #B #R #S #HRS #L2 #T1 #T2 #H elim H -T2 [ /3 width=3/ ]
 #T #T2 #_ #HT2 #IHT1 #L1 #HL12
 lapply (HRS … HT2 … HL12) -HRS -HT2 /3 width=3/