From 7593c0f74b944fb100493fb24b665ce3b8d1d252 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 21 Oct 2015 16:59:38 +0000
Subject: [PATCH] theory of multiple relocation completed

---
 .../cpys.ma => etc_new/cpys/cpys.etc}         |   0
 .../cpys_alt.ma => etc_new/cpys/cpys_alt.etc} |   0
 .../cpys/cpys_cpys.etc}                       |   0
 .../cpys/cpys_lift.etc}                       |   0
 .../llor.ma => etc_new/llor/llor.etc}         |   0
 .../llor_alt.ma => etc_new/llor/llor_alt.etc} |   0
 .../llor/llor_drop.etc}                       |   0
 .../lambdadelta/basic_2/multiple/lifts.ma     | 150 --------
 .../basic_2/multiple/lifts_lift.ma            |  63 ----
 .../basic_2/multiple/lifts_vector.ma          |  53 ---
 .../basic_2/{multiple => relocation}/drops.ma |   0
 .../{multiple => relocation}/drops_drop.ma    |   0
 .../{multiple => relocation}/drops_drops.ma   |   0
 .../basic_2/{multiple => relocation}/fleq.ma  |   0
 .../{multiple => relocation}/fleq_fleq.ma     |   0
 .../basic_2/{multiple => relocation}/fqup.ma  |   0
 .../{multiple => relocation}/fqup_fqup.ma     |   0
 .../basic_2/{multiple => relocation}/fqus.ma  |   0
 .../{multiple => relocation}/fqus_alt.ma      |   0
 .../{multiple => relocation}/fqus_fqus.ma     |   0
 .../lambdadelta/basic_2/relocation/frees.ma   |  41 +++
 .../lambdadelta/basic_2/relocation/lifts.ma   | 348 ++++++++++++++++++
 .../basic_2/relocation/lifts_lifts.ma         | 101 +++++
 .../basic_2/relocation/lifts_lifts_vector.ma  |  53 +++
 .../lifts_simple.ma}                          |  31 +-
 .../basic_2/relocation/lifts_vector.ma        | 114 ++++++
 .../lifts_weight.ma}                          |  16 +-
 .../basic_2/{multiple => relocation}/lleq.ma  |   0
 .../{multiple => relocation}/lleq_alt.ma      |   0
 .../{multiple => relocation}/lleq_alt_rec.ma  |   0
 .../{multiple => relocation}/lleq_drop.ma     |   0
 .../{multiple => relocation}/lleq_fqus.ma     |   0
 .../{multiple => relocation}/lleq_lleq.ma     |   0
 .../{multiple => relocation}/lleq_llor.ma     |   0
 .../{multiple => relocation}/lleq_lreq.ma     |   0
 .../{multiple => relocation}/llpx_sn.ma       |   0
 .../{multiple => relocation}/llpx_sn_alt.ma   |   0
 .../llpx_sn_alt_rec.ma                        |   0
 .../{multiple => relocation}/llpx_sn_drop.ma  |   0
 .../{multiple => relocation}/llpx_sn_frees.ma |   0
 .../{multiple => relocation}/llpx_sn_llor.ma  |   0
 .../llpx_sn_lpx_sn.ma                         |   0
 .../{multiple => relocation}/llpx_sn_lreq.ma  |   0
 .../{multiple => relocation}/llpx_sn_tc.ma    |   0
 44 files changed, 679 insertions(+), 291 deletions(-)
 rename matita/matita/contribs/lambdadelta/basic_2/{multiple/cpys.ma => etc_new/cpys/cpys.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{multiple/cpys_alt.ma => etc_new/cpys/cpys_alt.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{multiple/cpys_cpys.ma => etc_new/cpys/cpys_cpys.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{multiple/cpys_lift.ma => etc_new/cpys/cpys_lift.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{multiple/llor.ma => etc_new/llor/llor.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{multiple/llor_alt.ma => etc_new/llor/llor_alt.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{multiple/llor_drop.ma => etc_new/llor/llor_drop.etc} (100%)
 delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.ma
 delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lift.ma
 delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_vector.ma
 rename matita/matita/contribs/lambdadelta/basic_2/{multiple => relocation}/drops.ma (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{multiple => relocation}/drops_drop.ma (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{multiple => relocation}/drops_drops.ma (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{multiple => relocation}/fleq.ma (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{multiple => relocation}/fleq_fleq.ma (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{multiple => relocation}/fqup.ma (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{multiple => relocation}/fqup_fqup.ma (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{multiple => relocation}/fqus.ma (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{multiple => relocation}/fqus_alt.ma (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{multiple => relocation}/fqus_fqus.ma (100%)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/relocation/frees.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts_vector.ma
 rename matita/matita/contribs/lambdadelta/basic_2/{multiple/lifts_lift_vector.ma => relocation/lifts_simple.ma} (53%)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma
 rename matita/matita/contribs/lambdadelta/basic_2/{multiple/lifts_lifts.ma => relocation/lifts_weight.ma} (70%)
 rename matita/matita/contribs/lambdadelta/basic_2/{multiple => relocation}/lleq.ma (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{multiple => relocation}/lleq_alt.ma (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{multiple => relocation}/lleq_alt_rec.ma (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{multiple => relocation}/lleq_drop.ma (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{multiple => relocation}/lleq_fqus.ma (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{multiple => relocation}/lleq_lleq.ma (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{multiple => relocation}/lleq_llor.ma (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{multiple => relocation}/lleq_lreq.ma (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{multiple => relocation}/llpx_sn.ma (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{multiple => relocation}/llpx_sn_alt.ma (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{multiple => relocation}/llpx_sn_alt_rec.ma (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{multiple => relocation}/llpx_sn_drop.ma (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{multiple => relocation}/llpx_sn_frees.ma (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{multiple => relocation}/llpx_sn_llor.ma (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{multiple => relocation}/llpx_sn_lpx_sn.ma (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{multiple => relocation}/llpx_sn_lreq.ma (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{multiple => relocation}/llpx_sn_tc.ma (100%)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpys/cpys.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/multiple/cpys.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/cpys/cpys.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpys/cpys_alt.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_alt.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/cpys/cpys_alt.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpys/cpys_cpys.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_cpys.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/cpys/cpys_cpys.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpys/cpys_lift.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_lift.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/cpys/cpys_lift.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llor.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/llor/llor.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/multiple/llor.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/llor/llor.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llor_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/llor/llor_alt.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/multiple/llor_alt.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/llor/llor_alt.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llor_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/llor/llor_drop.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/multiple/llor_drop.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/llor/llor_drop.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.ma
deleted file mode 100644
index 7a091abce..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.ma
+++ /dev/null
@@ -1,150 +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/notation/relations/rliftstar_3.ma".
-include "basic_2/substitution/lift.ma".
-include "basic_2/multiple/mr2_plus.ma".
-
-(* GENERIC TERM RELOCATION **************************************************)
-
-inductive lifts: list2 ynat nat → relation term ≝
-| lifts_nil : ∀T. lifts (◊) T T
-| lifts_cons: ∀T1,T,T2,cs,l,m.
-              ⬆[l,m] T1 ≡ T → lifts cs T T2 → lifts ({l, m} @ cs) T1 T2
-.
-
-interpretation "generic relocation (term)"
-   'RLiftStar cs T1 T2 = (lifts cs T1 T2).
-
-(* Basic inversion lemmas ***************************************************)
-
-fact lifts_inv_nil_aux: ∀T1,T2,cs. ⬆*[cs] T1 ≡ T2 → cs = ◊ → T1 = T2.
-#T1 #T2 #cs * -T1 -T2 -cs //
-#T1 #T #T2 #l #m #cs #_ #_ #H destruct
-qed-.
-
-lemma lifts_inv_nil: ∀T1,T2. ⬆*[◊] T1 ≡ T2 → T1 = T2.
-/2 width=3 by lifts_inv_nil_aux/ qed-.
-
-fact lifts_inv_cons_aux: ∀T1,T2,cs. ⬆*[cs] T1 ≡ T2 →
-                         ∀l,m,tl. cs = {l, m} @ tl →
-                         ∃∃T. ⬆[l, m] T1 ≡ T & ⬆*[tl] T ≡ T2.
-#T1 #T2 #cs * -T1 -T2 -cs
-[ #T #l #m #tl #H destruct
-| #T1 #T #T2 #cs #l #m #HT1 #HT2 #l0 #m0 #tl #H destruct
-  /2 width=3 by ex2_intro/
-qed-.
-
-lemma lifts_inv_cons: ∀T1,T2,l,m,cs. ⬆*[{l, m} @ cs] T1 ≡ T2 →
-                      ∃∃T. ⬆[l, m] T1 ≡ T & ⬆*[cs] T ≡ T2.
-/2 width=3 by lifts_inv_cons_aux/ qed-.
-
-(* Basic_1: was: lift1_sort *)
-lemma lifts_inv_sort1: ∀T2,k,cs. ⬆*[cs] ⋆k ≡ T2 → T2 = ⋆k.
-#T2 #k #cs elim cs -cs
-[ #H <(lifts_inv_nil … H) -H //
-| #l #m #cs #IH #H
-  elim (lifts_inv_cons … H) -H #X #H
-  >(lift_inv_sort1 … H) -H /2 width=1 by/
-]
-qed-.
-
-(* Basic_1: was: lift1_lref *)
-lemma lifts_inv_lref1: ∀T2,cs,i1. ⬆*[cs] #i1 ≡ T2 →
-                       ∃∃i2. @⦃i1, cs⦄ ≡ i2 & T2 = #i2.
-#T2 #cs elim cs -cs
-[ #i1 #H <(lifts_inv_nil … H) -H /2 width=3 by at_nil, ex2_intro/
-| #l #m #cs #IH #i1 #H
-  elim (lifts_inv_cons … H) -H #X #H1 #H2
-  elim (lift_inv_lref1 … H1) -H1 * #Hli1 #H destruct
-  elim (IH … H2) -IH -H2 /3 width=3 by at_lt, at_ge, ex2_intro/
-]
-qed-.
-
-lemma lifts_inv_gref1: ∀T2,p,cs. ⬆*[cs] §p ≡ T2 → T2 = §p.
-#T2 #p #cs elim cs -cs
-[ #H <(lifts_inv_nil … H) -H //
-| #l #m #cs #IH #H
-  elim (lifts_inv_cons … H) -H #X #H
-  >(lift_inv_gref1 … H) -H /2 width=1 by/
-]
-qed-.
-
-(* Basic_1: was: lift1_bind *)
-lemma lifts_inv_bind1: ∀a,I,T2,cs,V1,U1. ⬆*[cs] ⓑ{a,I} V1. U1 ≡ T2 →
-                       ∃∃V2,U2. ⬆*[cs] V1 ≡ V2 & ⬆*[cs + 1] U1 ≡ U2 &
-                                T2 = ⓑ{a,I} V2. U2.
-#a #I #T2 #cs elim cs -cs
-[ #V1 #U1 #H
-  <(lifts_inv_nil … H) -H /2 width=5 by ex3_2_intro, lifts_nil/
-| #l #m #cs #IHcs #V1 #U1 #H
-  elim (lifts_inv_cons … H) -H #X #H #HT2
-  elim (lift_inv_bind1 … H) -H #V #U #HV1 #HU1 #H destruct
-  elim (IHcs … HT2) -IHcs -HT2 #V2 #U2 #HV2 #HU2 #H destruct
-  /3 width=5 by ex3_2_intro, lifts_cons/
-]
-qed-.
-
-(* Basic_1: was: lift1_flat *)
-lemma lifts_inv_flat1: ∀I,T2,cs,V1,U1. ⬆*[cs] ⓕ{I} V1. U1 ≡ T2 →
-                       ∃∃V2,U2. ⬆*[cs] V1 ≡ V2 & ⬆*[cs] U1 ≡ U2 &
-                                T2 = ⓕ{I} V2. U2.
-#I #T2 #cs elim cs -cs
-[ #V1 #U1 #H
-  <(lifts_inv_nil … H) -H /2 width=5 by ex3_2_intro, lifts_nil/
-| #l #m #cs #IHcs #V1 #U1 #H
-  elim (lifts_inv_cons … H) -H #X #H #HT2
-  elim (lift_inv_flat1 … H) -H #V #U #HV1 #HU1 #H destruct
-  elim (IHcs … HT2) -IHcs -HT2 #V2 #U2 #HV2 #HU2 #H destruct
-  /3 width=5 by ex3_2_intro, lifts_cons/
-]
-qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma lifts_simple_dx: ∀T1,T2,cs. ⬆*[cs] T1 ≡ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄.
-#T1 #T2 #cs #H elim H -T1 -T2 -cs /3 width=5 by lift_simple_dx/
-qed-.
-
-lemma lifts_simple_sn: ∀T1,T2,cs. ⬆*[cs] T1 ≡ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄.
-#T1 #T2 #cs #H elim H -T1 -T2 -cs /3 width=5 by lift_simple_sn/
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma lifts_bind: ∀a,I,T2,V1,V2,cs. ⬆*[cs] V1 ≡ V2 →
-                  ∀T1. ⬆*[cs + 1] T1 ≡ T2 →
-                  ⬆*[cs] ⓑ{a,I} V1. T1 ≡ ⓑ{a,I} V2. T2.
-#a #I #T2 #V1 #V2 #cs #H elim H -V1 -V2 -cs
-[ #V #T1 #H >(lifts_inv_nil … H) -H //
-| #V1 #V #V2 #cs #l #m #HV1 #_ #IHV #T1 #H
-  elim (lifts_inv_cons … H) -H /3 width=3 by lift_bind, lifts_cons/
-]
-qed.
-
-lemma lifts_flat: ∀I,T2,V1,V2,cs. ⬆*[cs] V1 ≡ V2 →
-                  ∀T1. ⬆*[cs] T1 ≡ T2 →
-                  ⬆*[cs] ⓕ{I} V1. T1 ≡ ⓕ{I} V2. T2.
-#I #T2 #V1 #V2 #cs #H elim H -V1 -V2 -cs
-[ #V #T1 #H >(lifts_inv_nil … H) -H //
-| #V1 #V #V2 #cs #l #m #HV1 #_ #IHV #T1 #H
-  elim (lifts_inv_cons … H) -H /3 width=3 by lift_flat, lifts_cons/
-]
-qed.
-
-lemma lifts_total: ∀cs,T1. ∃T2. ⬆*[cs] T1 ≡ T2.
-#cs elim cs -cs /2 width=2 by lifts_nil, ex_intro/
-#l #m #cs #IH #T1 elim (lift_total T1 l m)
-#T #HT1 elim (IH T) -IH /3 width=4 by lifts_cons, ex_intro/
-qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lift.ma
deleted file mode 100644
index 2c693baaa..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lift.ma
+++ /dev/null
@@ -1,63 +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 "ground_2/ynat/ynat_max.ma".
-include "basic_2/substitution/lift_lift.ma".
-include "basic_2/multiple/mr2_minus.ma".
-include "basic_2/multiple/lifts.ma".
-
-(* GENERIC TERM RELOCATION **************************************************)
-
-(* Properties concerning basic term relocation ******************************)
-
-(* Basic_1: was: lift1_xhg (right to left) *)
-lemma lifts_lift_trans_le: ∀T1,T,cs. ⬆*[cs] T1 ≡ T → ∀T2. ⬆[0, 1] T ≡ T2 →
-                           ∃∃T0. ⬆[0, 1] T1 ≡ T0 & ⬆*[cs + 1] T0 ≡ T2.
-#T1 #T #cs #H elim H -T1 -T -cs
-[ /2 width=3 by lifts_nil, ex2_intro/
-| #T1 #T3 #T #cs #l #m #HT13 #_ #IHT13 #T2 #HT2
-  elim (IHT13 … HT2) -T #T #HT3 #HT2
-  elim (lift_trans_le … HT13 … HT3) -T3 /3 width=5 by lifts_cons, ex2_intro/
-]
-qed-.
-
-(* Basic_1: was: lift1_free (right to left) *)
-lemma lifts_lift_trans: ∀cs,i,i0. @⦃i, cs⦄ ≡ i0 →
-                        ∀cs0. cs + 1 ▭ i + 1 ≡ cs0 + 1 →
-                        ∀T1,T0. ⬆*[cs0] T1 ≡ T0 →
-                        ∀T2. ⬆[O, i0 + 1] T0 ≡ T2 →
-                        ∃∃T. ⬆[0, i + 1] T1 ≡ T & ⬆*[cs] T ≡ T2.
-#cs elim cs -cs
-[ #i #x #H1 #cs0 #H2 #T1 #T0 #HT10 #T2
-  <(at_inv_nil … H1) -x #HT02
-  lapply (minuss_inv_nil1 … H2) -H2 #H
-  >(pluss_inv_nil2 … H) in HT10; -cs0 #H
-  >(lifts_inv_nil … H) -T1 /2 width=3 by lifts_nil, ex2_intro/
-| #l #m #cs #IHcs #i #i0 #H1 #cs0 #H2 #T1 #T0 #HT10 #T2 #HT02
-  elim (at_inv_cons … H1) -H1 * #Hil #Hi0
-  [ elim (minuss_inv_cons1_lt … H2) -H2 /2 width=1 by ylt_succ/ #cs1 #Hcs1
-    <yplus_inj >yplus_SO2 >yplus_SO2 >yminus_succ #H
-    elim (pluss_inv_cons2 … H) -H #cs2 #H1 #H2 destruct
-    elim (lifts_inv_cons … HT10) -HT10 #T #HT1 #HT0
-    elim (IHcs … Hi0 … Hcs1 … HT0 … HT02) -IHcs -Hi0 -Hcs1 -T0 #T0 #HT0 #HT02
-    elim (lift_trans_le … HT1 … HT0) -T /2 width=1 by/ #T #HT1
-    <yminus_plus2 <yplus_inj >yplus_SO2 >ymax_pre_sn
-    /3 width=5 by lifts_cons, ex2_intro, ylt_fwd_le_succ1/
-  | >commutative_plus in Hi0; #Hi0
-    lapply (minuss_inv_cons1_ge … H2 ?) -H2 /2 width=1 by yle_succ/ <associative_plus #Hcs0
-    elim (IHcs … Hi0 … Hcs0 … HT10 … HT02) -IHcs -Hi0 -Hcs0 -T0 #T0 #HT0 #HT02
-    elim (lift_split … HT0 l (i+1)) -HT0 /3 width=5 by lifts_cons, yle_succ, yle_pred_sn, ex2_intro/
-  ]
-]
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_vector.ma
deleted file mode 100644
index f98062e1e..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_vector.ma
+++ /dev/null
@@ -1,53 +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/substitution/lift_vector.ma".
-include "basic_2/multiple/lifts.ma".
-
-(* GENERIC TERM VECTOR RELOCATION *******************************************)
-
-inductive liftsv (cs:list2 ynat nat) : relation (list term) ≝
-| liftsv_nil : liftsv cs (◊) (◊)
-| liftsv_cons: ∀T1s,T2s,T1,T2.
-               ⬆*[cs] T1 ≡ T2 → liftsv cs T1s T2s →
-               liftsv cs (T1 @ T1s) (T2 @ T2s)
-.
-
-interpretation "generic relocation (vector)"
-   'RLiftStar cs T1s T2s = (liftsv cs T1s T2s).
-
-(* Basic inversion lemmas ***************************************************)
-
-(* Basic_1: was: lifts1_flat (left to right) *)
-lemma lifts_inv_applv1: ∀V1s,U1,T2,cs. ⬆*[cs] Ⓐ V1s. U1 ≡ T2 →
-                        ∃∃V2s,U2. ⬆*[cs] V1s ≡ V2s & ⬆*[cs] U1 ≡ U2 &
-                                  T2 = Ⓐ V2s. U2.
-#V1s elim V1s -V1s normalize
-[ #T1 #T2 #cs #HT12  
-  @ex3_2_intro [3,4: // |1,2: skip | // ] (**) (* explicit constructor *)
-| #V1 #V1s #IHV1s #T1 #X #cs #H
-  elim (lifts_inv_flat1 … H) -H #V2 #Y #HV12 #HY #H destruct
-  elim (IHV1s … HY) -IHV1s -HY #V2s #T2 #HV12s #HT12 #H destruct
-  @(ex3_2_intro) [4: // |3: /2 width=2 by liftsv_cons/ |1,2: skip | // ] (**) (* explicit constructor *)
-]
-qed-.
-
-(* Basic properties *********************************************************)
-
-(* Basic_1: was: lifts1_flat (right to left) *)
-lemma lifts_applv: ∀V1s,V2s,cs. ⬆*[cs] V1s ≡ V2s →
-                   ∀T1,T2. ⬆*[cs] T1 ≡ T2 →
-                   ⬆*[cs] Ⓐ V1s. T1 ≡ Ⓐ V2s. T2.
-#V1s #V2s #cs #H elim H -V1s -V2s /3 width=1 by lifts_flat/
-qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/drops.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/multiple/drops.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/drops_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_drop.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/multiple/drops_drop.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/drops_drop.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/drops_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_drops.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/multiple/drops_drops.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/drops_drops.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fleq.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/multiple/fleq.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/fleq.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/fleq_fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fleq_fleq.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/multiple/fleq_fleq.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/fleq_fleq.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fqup.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/multiple/fqup.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/fqup.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/fqup_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fqup_fqup.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/multiple/fqup_fqup.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/fqup_fqup.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fqus.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/multiple/fqus.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/fqus.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/fqus_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fqus_alt.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/multiple/fqus_alt.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/fqus_alt.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/fqus_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fqus_fqus.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/multiple/fqus_fqus.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/fqus_fqus.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/frees.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/frees.ma
new file mode 100644
index 000000000..15117986b
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/frees.ma
@@ -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/notation/relations/freestar_3.ma".
+include "basic_2/grammar/trace_sor.ma".
+include "basic_2/grammar/lenv.ma".
+
+(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
+
+inductive frees: relation3 lenv term trace ≝
+| frees_atom: ∀I. frees (⋆) (⓪{I}) (◊)
+| frees_sort: ∀L,k,cs. frees L (⋆k) cs →
+              ∀I,T. frees (L.ⓑ{I}T) (⋆k) (Ⓕ @ cs)
+| frees_zero: ∀L,T,cs. frees L T cs →
+              ∀I. frees (L.ⓑ{I}T) (#0) (Ⓣ @ cs)
+| frees_lref: ∀L,i,cs. frees L (#i) cs →
+              ∀I,T. frees (L.ⓑ{I}T) (#(S i)) (Ⓕ @ cs)
+| frees_gref: ∀L,p,cs. frees L (§p) cs →
+              ∀I,T. frees (L.ⓑ{I}T) (§p) (Ⓕ @ cs)
+| frees_bind: ∀cv,ct,cs. cv ⋓ ct ≡ cs →
+              ∀L,V. frees L V cv → ∀I,T,b. frees (L.ⓑ{I}V) T (b @ ct) →
+              ∀a. frees L (ⓑ{a,I}V.T) cs
+| frees_flat: ∀cv,ct,cs. cv ⋓ ct ≡ cs →
+              ∀L,V. frees L V cv → ∀T. frees L T ct →
+              ∀I. frees L (ⓕ{I}V.T) cs
+.
+
+interpretation
+   "context-sensitive free variables (term)"
+   'FreeStar L T cs = (frees L T cs).
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma
new file mode 100644
index 000000000..0ca46fa3c
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma
@@ -0,0 +1,348 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "ground_2/relocation/trace_isid.ma".
+include "basic_2/notation/relations/rliftstar_3.ma".
+include "basic_2/grammar/term.ma".
+
+(* GENERIC TERM RELOCATION **************************************************)
+
+(* Basic_1: includes:
+            lift_sort lift_lref_lt lift_lref_ge lift_bind lift_flat
+            lifts_nil lifts_cons
+*)
+inductive lifts: trace → relation term ≝
+| lifts_sort: ∀k,t. lifts t (⋆k) (⋆k)
+| lifts_lref: ∀i1,i2,t. @⦃i1, t⦄ ≡ i2 → lifts t (#i1) (#i2)
+| lifts_gref: ∀p,t. lifts t (§p) (§p)
+| lifts_bind: ∀a,I,V1,V2,T1,T2,t.
+              lifts t V1 V2 → lifts (Ⓣ@t) T1 T2 →
+              lifts t (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
+| lifts_flat: ∀I,V1,V2,T1,T2,t.
+              lifts t V1 V2 → lifts t T1 T2 →
+              lifts t (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
+.
+
+interpretation "generic relocation (term)"
+   'RLiftStar cs T1 T2 = (lifts cs T1 T2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lifts_inv_sort1_aux: ∀X,Y,t. ⬆*[t] X ≡ Y → ∀k. X = ⋆k → Y = ⋆k.
+#X #Y #t * -X -Y -t //
+[ #i1 #i2 #t #_ #x #H destruct
+| #a #I #V1 #V2 #T1 #T2 #t #_ #_ #x #H destruct
+| #I #V1 #V2 #T1 #T2 #t #_ #_ #x #H destruct
+]
+qed-.
+
+(* Basic_1: was: lift1_sort *)
+(* Basic_2A1: includes: lift_inv_sort1 *)
+lemma lifts_inv_sort1: ∀Y,k,t. ⬆*[t] ⋆k ≡ Y → Y = ⋆k.
+/2 width=4 by lifts_inv_sort1_aux/ qed-.
+
+fact lifts_inv_lref1_aux: ∀X,Y,t. ⬆*[t] X ≡ Y → ∀i1. X = #i1 →
+                          ∃∃i2. @⦃i1, t⦄ ≡ i2 & Y = #i2.
+#X #Y #t * -X -Y -t
+[ #k #t #x #H destruct
+| #i1 #i2 #t #Hi12 #x #H destruct /2 width=3 by ex2_intro/
+| #p #t #x #H destruct
+| #a #I #V1 #V2 #T1 #T2 #t #_ #_ #x #H destruct
+| #I #V1 #V2 #T1 #T2 #t #_ #_ #x #H destruct
+]
+qed-.
+
+(* Basic_1: was: lift1_lref *)
+(* Basic_2A1: includes: lift_inv_lref1 lift_inv_lref1_lt lift_inv_lref1_ge *)
+lemma lifts_inv_lref1: ∀Y,i1,t. ⬆*[t] #i1 ≡ Y →
+                       ∃∃i2. @⦃i1, t⦄ ≡ i2 & Y = #i2.
+/2 width=3 by lifts_inv_lref1_aux/ qed-.
+
+fact lifts_inv_gref1_aux: ∀X,Y,t. ⬆*[t] X ≡ Y → ∀p. X = §p → Y = §p.
+#X #Y #t * -X -Y -t //
+[ #i1 #i2 #t #_ #x #H destruct
+| #a #I #V1 #V2 #T1 #T2 #t #_ #_ #x #H destruct
+| #I #V1 #V2 #T1 #T2 #t #_ #_ #x #H destruct
+]
+qed-.
+
+(* Basic_2A1: includes: lift_inv_gref1 *)
+lemma lifts_inv_gref1: ∀Y,p,t. ⬆*[t] §p ≡ Y → Y = §p.
+/2 width=4 by lifts_inv_gref1_aux/ qed-.
+
+fact lifts_inv_bind1_aux: ∀X,Y,t. ⬆*[t] X ≡ Y →
+                          ∀a,I,V1,T1. X = ⓑ{a,I}V1.T1 →
+                          ∃∃V2,T2. ⬆*[t] V1 ≡ V2 & ⬆*[Ⓣ@t] T1 ≡ T2 &
+                                   Y = ⓑ{a,I}V2.T2.
+#X #Y #t * -X -Y -t
+[ #k #t #b #J #W1 #U1 #H destruct
+| #i1 #i2 #t #_ #b #J #W1 #U1 #H destruct
+| #p #t #b #J #W1 #U1 #H destruct
+| #a #I #V1 #V2 #T1 #T2 #t #HV12 #HT12 #b #J #W1 #U1 #H destruct /2 width=5 by ex3_2_intro/
+| #I #V1 #V2 #T1 #T2 #t #_ #_ #b #J #W1 #U1 #H destruct
+]
+qed-.
+
+(* Basic_1: was: lift1_bind *)
+(* Basic_2A1: includes: lift_inv_bind1 *)
+lemma lifts_inv_bind1: ∀a,I,V1,T1,Y,t. ⬆*[t] ⓑ{a,I}V1.T1 ≡ Y →
+                       ∃∃V2,T2. ⬆*[t] V1 ≡ V2 & ⬆*[Ⓣ@t] T1 ≡ T2 &
+                                Y = ⓑ{a,I}V2.T2.
+/2 width=3 by lifts_inv_bind1_aux/ qed-.
+
+fact lifts_inv_flat1_aux: ∀X,Y,t. ⬆*[t] X ≡ Y →
+                          ∀I,V1,T1. X = ⓕ{I}V1.T1 →
+                          ∃∃V2,T2. ⬆*[t] V1 ≡ V2 & ⬆*[t] T1 ≡ T2 &
+                                   Y = ⓕ{I}V2.T2.
+#X #Y #t * -X -Y -t
+[ #k #t #J #W1 #U1 #H destruct
+| #i1 #i2 #t #_ #J #W1 #U1 #H destruct
+| #p #t #J #W1 #U1 #H destruct
+| #a #I #V1 #V2 #T1 #T2 #t #_ #_ #J #W1 #U1 #H destruct
+| #I #V1 #V2 #T1 #T2 #t #HV12 #HT12 #J #W1 #U1 #H destruct /2 width=5 by ex3_2_intro/
+]
+qed-.
+
+(* Basic_1: was: lift1_flat *)
+(* Basic_2A1: includes: lift_inv_flat1 *)
+lemma lifts_inv_flat1: ∀I,V1,T1,Y,t. ⬆*[t] ⓕ{I}V1.T1 ≡ Y →
+                       ∃∃V2,T2. ⬆*[t] V1 ≡ V2 & ⬆*[t] T1 ≡ T2 &
+                                Y = ⓕ{I}V2.T2.
+/2 width=3 by lifts_inv_flat1_aux/ qed-.
+
+fact lifts_inv_sort2_aux: ∀X,Y,t. ⬆*[t] X ≡ Y → ∀k. Y = ⋆k → X = ⋆k.
+#X #Y #t * -X -Y -t //
+[ #i1 #i2 #t #_ #x #H destruct
+| #a #I #V1 #V2 #T1 #T2 #t #_ #_ #x #H destruct
+| #I #V1 #V2 #T1 #T2 #t #_ #_ #x #H destruct
+]
+qed-.
+
+(* Basic_1: includes: lift_gen_sort *)
+(* Basic_2A1: includes: lift_inv_sort2 *)
+lemma lifts_inv_sort2: ∀X,k,t. ⬆*[t] X ≡ ⋆k → X = ⋆k.
+/2 width=4 by lifts_inv_sort2_aux/ qed-.
+
+fact lifts_inv_lref2_aux: ∀X,Y,t. ⬆*[t] X ≡ Y → ∀i2. Y = #i2 →
+                          ∃∃i1. @⦃i1, t⦄ ≡ i2 & X = #i1.
+#X #Y #t * -X -Y -t
+[ #k #t #x #H destruct
+| #i1 #i2 #t #Hi12 #x #H destruct /2 width=3 by ex2_intro/
+| #p #t #x #H destruct
+| #a #I #V1 #V2 #T1 #T2 #t #_ #_ #x #H destruct
+| #I #V1 #V2 #T1 #T2 #t #_ #_ #x #H destruct
+]
+qed-.
+
+(* Basic_1: includes: lift_gen_lref lift_gen_lref_lt lift_gen_lref_false lift_gen_lref_ge *)
+(* Basic_2A1: includes: lift_inv_lref2 lift_inv_lref2_lt lift_inv_lref2_be lift_inv_lref2_ge lift_inv_lref2_plus *)
+lemma lifts_inv_lref2: ∀X,i2,t. ⬆*[t] X ≡ #i2 →
+                       ∃∃i1. @⦃i1, t⦄ ≡ i2 & X = #i1.
+/2 width=3 by lifts_inv_lref2_aux/ qed-.
+
+fact lifts_inv_gref2_aux: ∀X,Y,t. ⬆*[t] X ≡ Y → ∀p. Y = §p → X = §p.
+#X #Y #t * -X -Y -t //
+[ #i1 #i2 #t #_ #x #H destruct
+| #a #I #V1 #V2 #T1 #T2 #t #_ #_ #x #H destruct
+| #I #V1 #V2 #T1 #T2 #t #_ #_ #x #H destruct
+]
+qed-.
+
+(* Basic_2A1: includes: lift_inv_gref1 *)
+lemma lifts_inv_gref2: ∀X,p,t. ⬆*[t] X ≡ §p → X = §p.
+/2 width=4 by lifts_inv_gref2_aux/ qed-.
+
+fact lifts_inv_bind2_aux: ∀X,Y,t. ⬆*[t] X ≡ Y →
+                          ∀a,I,V2,T2. Y = ⓑ{a,I}V2.T2 →
+                          ∃∃V1,T1. ⬆*[t] V1 ≡ V2 & ⬆*[Ⓣ@t] T1 ≡ T2 &
+                                   X = ⓑ{a,I}V1.T1.
+#X #Y #t * -X -Y -t
+[ #k #t #b #J #W2 #U2 #H destruct
+| #i1 #i2 #t #_ #b #J #W2 #U2 #H destruct
+| #p #t #b #J #W2 #U2 #H destruct
+| #a #I #V1 #V2 #T1 #T2 #t #HV12 #HT12 #b #J #W2 #U2 #H destruct /2 width=5 by ex3_2_intro/
+| #I #V1 #V2 #T1 #T2 #t #_ #_ #b #J #W2 #U2 #H destruct
+]
+qed-.
+
+(* Basic_1: includes: lift_gen_bind *)
+(* Basic_2A1: includes: lift_inv_bind2 *)
+lemma lifts_inv_bind2: ∀a,I,V2,T2,X,t. ⬆*[t] X ≡ ⓑ{a,I}V2.T2 →
+                       ∃∃V1,T1. ⬆*[t] V1 ≡ V2 & ⬆*[Ⓣ@t] T1 ≡ T2 &
+                                X = ⓑ{a,I}V1.T1.
+/2 width=3 by lifts_inv_bind2_aux/ qed-.
+
+fact lifts_inv_flat2_aux: ∀X,Y,t. ⬆*[t] X ≡ Y →
+                          ∀I,V2,T2. Y = ⓕ{I}V2.T2 →
+                          ∃∃V1,T1. ⬆*[t] V1 ≡ V2 & ⬆*[t] T1 ≡ T2 &
+                                   X = ⓕ{I}V1.T1.
+#X #Y #t * -X -Y -t
+[ #k #t #J #W2 #U2 #H destruct
+| #i1 #i2 #t #_ #J #W2 #U2 #H destruct
+| #p #t #J #W2 #U2 #H destruct
+| #a #I #V1 #V2 #T1 #T2 #t #_ #_ #J #W2 #U2 #H destruct
+| #I #V1 #V2 #T1 #T2 #t #HV12 #HT12 #J #W2 #U2 #H destruct /2 width=5 by ex3_2_intro/
+]
+qed-.
+
+(* Basic_1: includes: lift_gen_flat *)
+(* Basic_2A1: includes: lift_inv_flat2 *)
+lemma lifts_inv_flat2: ∀I,V2,T2,X,t. ⬆*[t] X ≡ ⓕ{I}V2.T2 →
+                       ∃∃V1,T1. ⬆*[t] V1 ≡ V2 & ⬆*[t] T1 ≡ T2 &
+                                X = ⓕ{I}V1.T1.
+/2 width=3 by lifts_inv_flat2_aux/ qed-.
+
+(* Basic_2A1: includes: lift_inv_pair_xy_x *)
+lemma lifts_inv_pair_xy_x: ∀I,V,T,t. ⬆*[t] ②{I}V.T ≡ V → ⊥.
+#J #V elim V -V
+[ * #i #U #t #H
+  [ lapply (lifts_inv_sort2 … H) -H #H destruct
+  | elim (lifts_inv_lref2 … H) -H
+    #x #_ #H destruct
+  | lapply (lifts_inv_gref2 … H) -H #H destruct
+  ]
+| * [ #a ] #I #V2 #T2 #IHV2 #_ #U #t #H
+  [ elim (lifts_inv_bind2 … H) -H #V1 #T1 #HV12 #_ #H destruct /2 width=3 by/
+  | elim (lifts_inv_flat2 … H) -H #V1 #T1 #HV12 #_ #H destruct /2 width=3 by/
+  ]
+]
+qed-.
+
+(* Basic_1: includes: thead_x_lift_y_y *)
+(* Basic_2A1: includes: lift_inv_pair_xy_y *)
+lemma lifts_inv_pair_xy_y: ∀I,T,V,t. ⬆*[t] ②{I}V.T ≡ T → ⊥.
+#J #T elim T -T
+[ * #i #W #t #H
+  [ lapply (lifts_inv_sort2 … H) -H #H destruct
+  | elim (lifts_inv_lref2 … H) -H
+    #x #_ #H destruct
+  | lapply (lifts_inv_gref2 … H) -H #H destruct
+  ]
+| * [ #a ] #I #V2 #T2 #_ #IHT2 #W #t #H
+  [ elim (lifts_inv_bind2 … H) -H #V1 #T1 #_ #HT12 #H destruct /2 width=4 by/
+  | elim (lifts_inv_flat2 … H) -H #V1 #T1 #_ #HT12 #H destruct /2 width=4 by/
+  ]
+]
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+(* Basic_2A1: includes: lift_inv_O2 *)
+lemma lifts_fwd_isid: ∀T1,T2,t. ⬆*[t] T1 ≡ T2 → 𝐈⦃t⦄ → T1 = T2.
+#T1 #T2 #t #H elim H -T1 -T2 -t /4 width=3 by isid_inv_at, eq_f2, eq_f/
+qed-.
+
+(* Basic_2A1: includes: lift_fwd_pair1 *)
+lemma lifts_fwd_pair1: ∀I,V1,T1,Y,t. ⬆*[t] ②{I}V1.T1 ≡ Y →
+                       ∃∃V2,T2. ⬆*[t] V1 ≡ V2 & Y = ②{I}V2.T2.
+* [ #a ] #I #V1 #T1 #Y #t #H
+[ elim (lifts_inv_bind1 … H) -H /2 width=4 by ex2_2_intro/
+| elim (lifts_inv_flat1 … H) -H /2 width=4 by ex2_2_intro/
+]
+qed-.
+
+(* Basic_2A1: includes: lift_fwd_pair2 *)
+lemma lifts_fwd_pair2: ∀I,V2,T2,X,t. ⬆*[t] X ≡ ②{I}V2.T2 →
+                       ∃∃V1,T1. ⬆*[t] V1 ≡ V2 & X = ②{I}V1.T1.
+* [ #a ] #I #V2 #T2 #X #t #H
+[ elim (lifts_inv_bind2 … H) -H /2 width=4 by ex2_2_intro/
+| elim (lifts_inv_flat2 … H) -H /2 width=4 by ex2_2_intro/
+]
+qed-.
+
+(* Basic properties *********************************************************)
+
+(* Basic_1: includes: lift_free (right to left) *)
+(* Basic_2A1: includes: lift_split *)
+lemma lifts_split_trans: ∀T1,T2,t. ⬆*[t] T1 ≡ T2 →
+                         ∀t1,t2. t2 ⊚ t1 ≡ t →
+                         ∃∃T. ⬆*[t1] T1 ≡ T & ⬆*[t2] T ≡ T2.
+#T1 #T2 #t #H elim H -T1 -T2 -t
+[ /3 width=3 by lifts_sort, ex2_intro/
+| #i1 #i2 #t #Hi #t1 #t2 #Ht elim (after_at_fwd … Ht … Hi) -Ht -Hi
+  /3 width=3 by lifts_lref, ex2_intro/
+| /3 width=3 by lifts_gref, ex2_intro/
+| #a #I #V1 #V2 #T1 #T2 #t #_ #_ #IHV #IHT #t1 #t2 #Ht
+  elim (IHV … Ht) elim (IHT (Ⓣ@t1) (Ⓣ@t2)) -IHV -IHT
+  /3 width=5 by lifts_bind, after_true, ex2_intro/
+| #I #V1 #V2 #T1 #T2 #t #_ #_ #IHV #IHT #t1 #t2 #Ht
+  elim (IHV … Ht) elim (IHT … Ht) -IHV -IHT -Ht
+  /3 width=5 by lifts_flat, ex2_intro/
+]
+qed-.
+
+(* Note: apparently, this was missing in Basic_2A1 *)
+lemma lifts_split_div: ∀T1,T2,t1. ⬆*[t1] T1 ≡ T2 →
+                       ∀t2,t. t2 ⊚ t1 ≡ t →
+                       ∃∃T. ⬆*[t2] T2 ≡ T & ⬆*[t] T1 ≡ T.
+#T1 #T2 #t1 #H elim H -T1 -T2 -t1
+[ /3 width=3 by lifts_sort, ex2_intro/
+| #i1 #i2 #t1 #Hi #t2 #t #Ht elim (after_at1_fwd … Ht … Hi) -Ht -Hi
+  /3 width=3 by lifts_lref, ex2_intro/
+| /3 width=3 by lifts_gref, ex2_intro/
+| #a #I #V1 #V2 #T1 #T2 #t1 #_ #_ #IHV #IHT #t2 #t #Ht
+  elim (IHV … Ht) elim (IHT (Ⓣ@t2) (Ⓣ@t)) -IHV -IHT
+  /3 width=5 by lifts_bind, after_true, ex2_intro/
+| #I #V1 #V2 #T1 #T2 #t1 #_ #_ #IHV #IHT #t2 #t #Ht
+  elim (IHV … Ht) elim (IHT … Ht) -IHV -IHT -Ht
+  /3 width=5 by lifts_flat, ex2_intro/
+]
+qed-.
+
+(* Basic_1: includes: dnf_dec2 dnf_dec *)
+(* Basic_2A1: includes: is_lift_dec *)
+lemma is_lifts_dec: ∀T2,t. Decidable (∃T1. ⬆*[t] T1 ≡ T2).
+#T1 elim T1 -T1
+[ * [1,3: /3 width=2 by lifts_sort, lifts_gref, ex_intro, or_introl/ ]
+  #i2 #t elim (is_at_dec t i2)
+  [ * /4 width=3 by lifts_lref, ex_intro, or_introl/
+  | #H @or_intror *
+    #X #HX elim (lifts_inv_lref2 … HX) -HX
+    /3 width=2 by ex_intro/
+  ]
+| * [ #a ] #I #V2 #T2 #IHV2 #IHT2 #t
+  [ elim (IHV2 t) -IHV2
+    [ * #V1 #HV12 elim (IHT2 (Ⓣ@t)) -IHT2
+      [ * #T1 #HT12 @or_introl /3 width=2 by lifts_bind, ex_intro/
+      | -V1 #HT2 @or_intror * #X #H
+        elim (lifts_inv_bind2 … H) -H /3 width=2 by ex_intro/
+      ]
+    | -IHT2 #HV2 @or_intror * #X #H
+      elim (lifts_inv_bind2 … H) -H /3 width=2 by ex_intro/
+    ]
+  | elim (IHV2 t) -IHV2
+    [ * #V1 #HV12 elim (IHT2 t) -IHT2
+      [ * #T1 #HT12 /4 width=2 by lifts_flat, ex_intro, or_introl/
+      | -V1 #HT2 @or_intror * #X #H
+        elim (lifts_inv_flat2 … H) -H /3 width=2 by ex_intro/
+      ]
+    | -IHT2 #HV2 @or_intror * #X #H
+      elim (lifts_inv_flat2 … H) -H /3 width=2 by ex_intro/
+    ]
+  ]
+]
+qed-.
+
+(* Basic_2A1: removed theorems 17:
+              lifts_inv_nil lifts_inv_cons lifts_total
+              lift_inv_Y1 lift_inv_Y2 lift_inv_lref_Y1 lift_inv_lref_Y2 lift_lref_Y lift_Y1
+              lift_lref_lt_eq lift_lref_ge_eq lift_lref_plus lift_lref_pred
+              lift_lref_ge_minus lift_lref_ge_minus_eq lift_total lift_refl
+*)
+(* Basic_1: removed theorems 8:
+            lift_lref_gt            
+            lift_head lift_gen_head 
+            lift_weight_map lift_weight lift_weight_add lift_weight_add_O
+            lift_tlt_dx
+*)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma
new file mode 100644
index 000000000..b0e32002c
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma
@@ -0,0 +1,101 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/lifts.ma".
+
+(* GENERIC RELOCATION *******************************************************)
+
+(* Main properties **********************************************************)
+
+(* Basic_2A1: includes: lift_inj *)
+theorem lifts_inj: ∀t,T1,U. ⬆*[t] T1 ≡ U → ∀T2. ⬆*[t] T2 ≡ U → T1 = T2.
+#t #T1 #U #H elim H -t -T1 -U
+[ /2 width=2 by lifts_inv_sort2/
+| #i1 #j #t #Hi1j #X #HX elim (lifts_inv_lref2 … HX) -HX
+  /4 width=4 by at_inj, eq_f/
+| /2 width=2 by lifts_inv_gref2/
+| #a #I #V1 #V2 #T1 #T2 #t #_ #_ #IHV12 #IHT12 #X #HX elim (lifts_inv_bind2 … HX) -HX
+  #V #T #HV1 #HT1 #HX destruct /3 width=1 by eq_f2/
+| #I #V1 #V2 #T1 #T2 #t #_ #_ #IHV12 #IHT12 #X #HX elim (lifts_inv_flat2 … HX) -HX
+  #V #T #HV1 #HT1 #HX destruct /3 width=1 by eq_f2/
+]
+qed-.
+
+(* Basic_1: includes: lift_gen_lift *)
+(* Basic_2A1: includes: lift_div_le lift_div_be *)
+theorem lifts_div: ∀T,T2,t2. ⬆*[t2] T2 ≡ T → ∀T1,t. ⬆*[t] T1 ≡ T →
+                   ∀t1. t2 ⊚ t1 ≡ t → ⬆*[t1] T1 ≡ T2.
+#T #T2 #t2 #H elim H -T -T2 -t2
+[ #k #t2 #T1 #t #H >(lifts_inv_sort2 … H) -T1 //
+| #i2 #i #t2 #Hi2 #T1 #t #H #t1 #Ht21 elim (lifts_inv_lref2 … H) -H
+  #i1 #Hi1 #H destruct /3 width=6 by lifts_lref, after_fwd_at1/
+| #p #t2 #T1 #t #H >(lifts_inv_gref2 … H) -T1 //
+| #a #I #W2 #W #U2 #U #t2 #_ #_ #IHW #IHU #T1 #t #H
+  elim (lifts_inv_bind2 … H) -H #W1 #U1 #HW1 #HU1 #H destruct
+  /4 width=3 by lifts_bind, after_true/
+| #I #W2 #W #U2 #U #t2 #_ #_ #IHW #IHU #T1 #t #H
+  elim (lifts_inv_flat2 … H) -H #W1 #U1 #HW1 #HU1 #H destruct
+  /3 width=3 by lifts_flat/
+]
+qed-.
+
+(* Basic_2A1: includes: lift_mono *)
+theorem lifts_mono: ∀t,T,U1. ⬆*[t] T ≡ U1 → ∀U2. ⬆*[t] T ≡ U2 → U1 = U2.
+#t #T #U1 #H elim H -t -T -U1
+[ /2 width=2 by lifts_inv_sort1/
+| #i1 #j #t #Hi1j #X #HX elim (lifts_inv_lref1 … HX) -HX
+  /4 width=4 by at_mono, eq_f/
+| /2 width=2 by lifts_inv_gref1/
+| #a #I #V1 #V2 #T1 #T2 #t #_ #_ #IHV12 #IHT12 #X #HX elim (lifts_inv_bind1 … HX) -HX
+  #V #T #HV1 #HT1 #HX destruct /3 width=1 by eq_f2/
+| #I #V1 #V2 #T1 #T2 #t #_ #_ #IHV12 #IHT12 #X #HX elim (lifts_inv_flat1 … HX) -HX
+  #V #T #HV1 #HT1 #HX destruct /3 width=1 by eq_f2/
+]
+qed-.
+
+(* Basic_1: was: lift1_lift1 (left to right) *)
+(* Basic_1: includes: lift_free (left to right) lift_d lift1_xhg (right to left) lift1_free (right to left) *)
+(* Basic_2A1: includes: lift_trans_be lift_trans_le lift_trans_ge lifts_lift_trans_le lifts_lift_trans *)
+theorem lifts_trans: ∀T1,T,t1. ⬆*[t1] T1 ≡ T → ∀T2,t2. ⬆*[t2] T ≡ T2 →
+                     ∀t. t2 ⊚ t1 ≡ t → ⬆*[t] T1 ≡ T2.
+#T1 #T #t1 #H elim H -T1 -T -t1
+[ #k #t1 #T2 #t2 #H >(lifts_inv_sort1 … H) -T2 //
+| #i1 #i #t1 #Hi1 #T2 #t2 #H #t #Ht21 elim (lifts_inv_lref1 … H) -H
+  #i2 #Hi2 #H destruct /3 width=6 by lifts_lref, after_fwd_at/
+| #p #t1 #T2 #t2 #H >(lifts_inv_gref1 … H) -T2 //
+| #a #I #W1 #W #U1 #U #t1 #_ #_ #IHW #IHU #T2 #t2 #H
+  elim (lifts_inv_bind1 … H) -H #W2 #U2 #HW2 #HU2 #H destruct
+  /4 width=3 by lifts_bind, after_true/
+| #I #W1 #W #U1 #U #t1 #_ #_ #IHW #IHU #T2 #t2 #H
+  elim (lifts_inv_flat1 … H) -H #W2 #U2 #HW2 #HU2 #H destruct
+  /3 width=3 by lifts_flat/
+]
+qed-.
+
+(* Basic_2A1: includes: lift_conf_O1 lift_conf_be *)
+theorem lifts_conf: ∀T,T1,t1. ⬆*[t1] T ≡ T1 → ∀T2,t. ⬆*[t] T ≡ T2 →
+                    ∀t2. t2 ⊚ t1 ≡ t → ⬆*[t2] T1 ≡ T2.
+#T #T1 #t1 #H elim H -T -T1 -t1
+[ #k #t1 #T2 #t #H >(lifts_inv_sort1 … H) -T2 //
+| #i #i1 #t1 #Hi1 #T2 #t #H #t2 #Ht21 elim (lifts_inv_lref1 … H) -H
+  #i2 #Hi2 #H destruct /3 width=6 by lifts_lref, after_fwd_at2/
+| #p #t1 #T2 #t #H >(lifts_inv_gref1 … H) -T2 //
+| #a #I #W #W1 #U #U1 #t1 #_ #_ #IHW #IHU #T2 #t #H
+  elim (lifts_inv_bind1 … H) -H #W2 #U2 #HW2 #HU2 #H destruct
+  /4 width=3 by lifts_bind, after_true/
+| #I #W #W1 #U #U1 #t1 #_ #_ #IHW #IHU #T2 #t #H
+  elim (lifts_inv_flat1 … H) -H #W2 #U2 #HW2 #HU2 #H destruct
+  /3 width=3 by lifts_flat/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts_vector.ma
new file mode 100644
index 000000000..fb5953c26
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts_vector.ma
@@ -0,0 +1,53 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/lifts_lifts.ma".
+include "basic_2/relocation/lifts_vector.ma".
+
+(* GENERIC TERM VECTOR RELOCATION *******************************************)
+
+(* Main properties **********************************************************)
+
+(* Basic_1: includes: lifts_inj *)
+theorem liftsv_inj: ∀T1s,Us,t. ⬆*[t] T1s ≡ Us →
+                    ∀T2s. ⬆*[t] T2s ≡ Us → T1s = T2s.
+#T1s #Us #t #H elim H -T1s -Us
+[ #T2s #H >(liftsv_inv_nil2 … H) -H //
+| #T1s #Us #T1 #U #HT1U #_ #IHT1Us #X #H destruct
+  elim (liftsv_inv_cons2 … H) -H #T2 #T2s #HT2U #HT2Us #H destruct
+  >(lifts_inj … HT1U … HT2U) -U /3 width=1 by eq_f/
+]
+qed-.
+
+(* Basic_2A1: includes: liftv_mono *)
+theorem liftsv_mono: ∀Ts,U1s,t. ⬆*[t] Ts ≡ U1s →
+                     ∀U2s. ⬆*[t] Ts ≡ U2s → U1s = U2s.
+#Ts #U1s #t #H elim H -Ts -U1s
+[ #U2s #H >(liftsv_inv_nil1 … H) -H //
+| #Ts #U1s #T #U1 #HTU1 #_ #IHTU1s #X #H destruct
+  elim (liftsv_inv_cons1 … H) -H #U2 #U2s #HTU2 #HTU2s #H destruct
+  >(lifts_mono … HTU1 … HTU2) -T /3 width=1 by eq_f/
+]
+qed-.
+
+(* Basic_1: includes: lifts1_xhg (right to left) *)
+(* Basic_2A1: includes: liftsv_liftv_trans_le *)
+theorem liftsv_trans: ∀T1s,Ts,t1. ⬆*[t1] T1s ≡ Ts → ∀T2s,t2. ⬆*[t2] Ts ≡ T2s →
+                      ∀t. t2 ⊚ t1 ≡ t → ⬆*[t] T1s ≡ T2s.
+#T1s #Ts #t1 #H elim H -T1s -Ts
+[ #T2s #t2 #H >(liftsv_inv_nil1 … H) -T2s /2 width=3 by liftsv_nil/
+| #T1s #Ts #T1 #T #HT1 #_ #IHT1s #X #t2 #H elim (liftsv_inv_cons1 … H) -H
+  #T2 #T2s #HT2 #HT2s #H destruct /3 width=6 by lifts_trans, liftsv_cons/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lift_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_simple.ma
similarity index 53%
rename from matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lift_vector.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_simple.ma
index e09e0f00a..389f724d2 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lift_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_simple.ma
@@ -12,24 +12,21 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/lift_lift_vector.ma".
-include "basic_2/multiple/lifts_lift.ma".
-include "basic_2/multiple/lifts_vector.ma".
+include "basic_2/grammar/term_simple.ma".
+include "basic_2/relocation/lifts.ma".
 
-(* GENERIC RELOCATION *******************************************************)
+(* GENERIC TERM RELOCATION **************************************************)
 
-(* Main properties **********************************************************)
+(* Forward lemmas on simple terms *******************************************)
 
-(* Basic_1: was: lifts1_xhg (right to left) *)
-lemma liftsv_liftv_trans_le: ∀T1s,Ts,cs. ⬆*[cs] T1s ≡ Ts →
-                             ∀T2s:list term. ⬆[0, 1] Ts ≡ T2s →
-                             ∃∃T0s. ⬆[0, 1] T1s ≡ T0s & ⬆*[cs + 1] T0s ≡ T2s.
-#T1s #Ts #cs #H elim H -T1s -Ts
-[ #T1s #H
-  >(liftv_inv_nil1 … H) -T1s /2 width=3 by liftsv_nil, liftv_nil, ex2_intro/
-| #T1s #Ts #T1 #T #HT1 #_ #IHT1s #X #H
-  elim (liftv_inv_cons1 … H) -H #T2 #T2s #HT2 #HT2s #H destruct
-  elim (IHT1s … HT2s) -Ts #Ts #HT1s #HT2s
-  elim (lifts_lift_trans_le … HT1 … HT2) -T /3 width=5 by liftsv_cons, liftv_cons, ex2_intro/
-]
+(* Basic_2A1: includes: lift_simple_dx *)
+lemma lifts_simple_dx: ∀T1,T2,t. ⬆*[t] T1 ≡ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄.
+#T1 #T2 #t #H elim H -T1 -T2 -t //
+#a #I #V1 #V2 #T1 #T2 #t #_ #_ #_ #_ #H elim (simple_inv_bind … H)
+qed-.
+
+(* Basic_2A1: includes: lift_simple_sn *)
+lemma lifts_simple_sn: ∀T1,T2,t. ⬆*[t] T1 ≡ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄.
+#T1 #T2 #t #H elim H -T1 -T2 -t //
+#a #I #V1 #V2 #T1 #T2 #t #_ #_ #_ #_ #H elim (simple_inv_bind … H)
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma
new file mode 100644
index 000000000..89ead4cf5
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma
@@ -0,0 +1,114 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/term_vector.ma".
+include "basic_2/relocation/lifts.ma".
+
+(* GENERIC TERM VECTOR RELOCATION *******************************************)
+
+(* Basic_2A1: includes: liftv_nil liftv_cons *)
+inductive liftsv (t:trace) : relation (list term) ≝
+| liftsv_nil : liftsv t (◊) (◊)
+| liftsv_cons: ∀T1s,T2s,T1,T2.
+               ⬆*[t] T1 ≡ T2 → liftsv t T1s T2s →
+               liftsv t (T1 @ T1s) (T2 @ T2s)
+.
+
+interpretation "generic relocation (vector)"
+   'RLiftStar t T1s T2s = (liftsv t T1s T2s).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact liftsv_inv_nil1_aux: ∀X,Y,t. ⬆*[t] X ≡ Y → X = ◊ → Y = ◊.
+#X #Y #t * -X -Y //
+#T1s #T2s #T1 #T2 #_ #_ #H destruct
+qed-.
+
+(* Basic_2A1: includes: liftv_inv_nil1 *)
+lemma liftsv_inv_nil1: ∀Y,t. ⬆*[t] ◊ ≡ Y → Y = ◊.
+/2 width=5 by liftsv_inv_nil1_aux/ qed-.
+
+fact liftsv_inv_cons1_aux: ∀X,Y,t. ⬆*[t] X ≡ Y →
+                           ∀T1,T1s. X = T1 @ T1s →
+                           ∃∃T2,T2s. ⬆*[t] T1 ≡ T2 & ⬆*[t] T1s ≡ T2s &
+                                     Y = T2 @ T2s.
+#X #Y #t * -X -Y
+[ #U1 #U1s #H destruct
+| #T1s #T2s #T1 #T2 #HT12 #HT12s #U1 #U1s #H destruct /2 width=5 by ex3_2_intro/
+]
+qed-.
+
+(* Basic_2A1: includes: liftv_inv_cons1 *)
+lemma liftsv_inv_cons1: ∀T1,T1s,Y,t. ⬆*[t] T1 @ T1s ≡ Y →
+                        ∃∃T2,T2s. ⬆*[t] T1 ≡ T2 & ⬆*[t] T1s ≡ T2s &
+                                  Y = T2 @ T2s.
+/2 width=3 by liftsv_inv_cons1_aux/ qed-.
+
+fact liftsv_inv_nil2_aux: ∀X,Y,t. ⬆*[t] X ≡ Y → Y = ◊ → X = ◊.
+#X #Y #t * -X -Y //
+#T1s #T2s #T1 #T2 #_ #_ #H destruct
+qed-.
+
+lemma liftsv_inv_nil2: ∀X,t. ⬆*[t] X ≡ ◊ → X = ◊.
+/2 width=5 by liftsv_inv_nil2_aux/ qed-.
+
+fact liftsv_inv_cons2_aux: ∀X,Y,t. ⬆*[t] X ≡ Y →
+                           ∀T2,T2s. Y = T2 @ T2s →
+                           ∃∃T1,T1s. ⬆*[t] T1 ≡ T2 & ⬆*[t] T1s ≡ T2s &
+                                     X = T1 @ T1s.
+#X #Y #t * -X -Y
+[ #U2 #U2s #H destruct
+| #T1s #T2s #T1 #T2 #HT12 #HT12s #U2 #U2s #H destruct /2 width=5 by ex3_2_intro/
+]
+qed-.
+
+lemma liftsv_inv_cons2: ∀X,T2,T2s,t. ⬆*[t] X ≡ T2 @ T2s →
+                        ∃∃T1,T1s. ⬆*[t] T1 ≡ T2 & ⬆*[t] T1s ≡ T2s &
+                                  X = T1 @ T1s.
+/2 width=3 by liftsv_inv_cons2_aux/ qed-.
+
+(* Basic_1: was: lifts1_flat (left to right) *)
+lemma lifts_inv_applv1: ∀V1s,U1,T2,t. ⬆*[t] Ⓐ V1s.U1 ≡ T2 →
+                        ∃∃V2s,U2. ⬆*[t] V1s ≡ V2s & ⬆*[t] U1 ≡ U2 &
+                                  T2 = Ⓐ V2s.U2.
+#V1s elim V1s -V1s
+[ /3 width=5 by ex3_2_intro, liftsv_nil/
+| #V1 #V1s #IHV1s #T1 #X #t #H elim (lifts_inv_flat1 … H) -H
+  #V2 #Y #HV12 #HY #H destruct elim (IHV1s … HY) -IHV1s -HY
+  #V2s #T2 #HV12s #HT12 #H destruct /3 width=5 by ex3_2_intro, liftsv_cons/
+]
+qed-.
+
+lemma lifts_inv_applv2: ∀V2s,U2,T1,t. ⬆*[t] T1 ≡ Ⓐ V2s.U2 →
+                        ∃∃V1s,U1. ⬆*[t] V1s ≡ V2s & ⬆*[t] U1 ≡ U2 &
+                                  T1 = Ⓐ V1s.U1.
+#V2s elim V2s -V2s
+[ /3 width=5 by ex3_2_intro, liftsv_nil/
+| #V2 #V2s #IHV2s #T2 #X #t #H elim (lifts_inv_flat2 … H) -H
+  #V1 #Y #HV12 #HY #H destruct elim (IHV2s … HY) -IHV2s -HY
+  #V1s #T1 #HV12s #HT12 #H destruct /3 width=5 by ex3_2_intro, liftsv_cons/
+]
+qed-.
+
+(* Basic properties *********************************************************)
+
+(* Basic_1: was: lifts1_flat (right to left) *)
+lemma lifts_applv: ∀V1s,V2s,t. ⬆*[t] V1s ≡ V2s →
+                   ∀T1,T2. ⬆*[t] T1 ≡ T2 →
+                   ⬆*[t] Ⓐ V1s. T1 ≡ Ⓐ V2s. T2.
+#V1s #V2s #t #H elim H -V1s -V2s /3 width=1 by lifts_flat/
+qed.
+
+(* Basic_2A1: removed theorems 1: liftv_total *)
+(* Basic_1: removed theorems 2: lifts1_nil lifts1_cons *)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_weight.ma
similarity index 70%
rename from matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lifts.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_weight.ma
index cff6bf238..17952bba8 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lifts.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_weight.ma
@@ -12,14 +12,14 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/multiple/lifts_lift.ma".
+include "basic_2/grammar/term_weight.ma".
+include "basic_2/relocation/lifts.ma".
 
-(* GENERIC RELOCATION *******************************************************)
+(* GENERIC TERM RELOCATION **************************************************)
 
-(* Main properties **********************************************************)
+(* Forward lemmas on weight for terms ***************************************)
 
-(* Basic_1: was: lift1_lift1 (left to right) *)
-theorem lifts_trans: ∀T1,T,cs1. ⬆*[cs1] T1 ≡ T → ∀T2:term. ∀cs2. ⬆*[cs2] T ≡ T2 →
-                     ⬆*[cs1 @@ cs2] T1 ≡ T2.
-#T1 #T #cs1 #H elim H -T1 -T -cs1 /3 width=3 by lifts_cons/
-qed.
+(* Basic_2A1: includes: lift_fwd_tw *)
+lemma lifts_fwd_tw: ∀T1,T2,t. ⬆*[t] T1 ≡ T2 → ♯{T1} = ♯{T2}.
+#T1 #T2 #t #H elim H -T1 -T2 -t normalize //
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/multiple/lleq.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/lleq.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_alt.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_alt.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_alt.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_alt_rec.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_alt_rec.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_alt_rec.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_alt_rec.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_drop.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_drop.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_drop.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_fqus.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_fqus.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_fqus.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_lleq.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_lleq.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_lleq.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_llor.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_llor.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_llor.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_llor.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_lreq.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_lreq.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_lreq.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_alt.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_alt.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_alt.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_alt_rec.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_alt_rec.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_alt_rec.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_alt_rec.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_drop.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_drop.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_drop.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_frees.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_frees.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_frees.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_frees.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_llor.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_llor.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_llor.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_llor.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_lpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_lpx_sn.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_lpx_sn.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_lpx_sn.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_lreq.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_lreq.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_lreq.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_tc.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_tc.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_tc.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_tc.ma
-- 
2.39.2