From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 16 Jan 2014 21:49:29 +0000 (+0000)
Subject: commit of the "relocation" component with the new definition of ldrop,
X-Git-Tag: make_still_working~998
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=928cfe1ebf2fbd31731c8851cdec70802596016d;p=helm.git

commit of the "relocation" component with the new definition of ldrop,
the other components will be committed shortly ...
---

diff --git a/matita/matita/contribs/lambdadelta/basic_2/names.txt b/matita/matita/contribs/lambdadelta/basic_2/names.txt
index 1bfe7ed6d..a9008510e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/names.txt
+++ b/matita/matita/contribs/lambdadelta/basic_2/names.txt
@@ -28,7 +28,8 @@ l      : term degree
 m,n    : reserved: future use
 o      :
 p,q    : global reference position
-r,s    :
+r      : reduction kind parameter (true = ordinary, false = extended)
+s      : local dropping kind parameter (true = general, false = restricted)
 t,u    : local reference position level (de Bruijn's)
 v,w    :
 x,y,z  : reserved: transient objet denoted by a small letter
@@ -39,6 +40,8 @@ NAMING CONVENTIONS FOR CONSTRUCTORS
 2: binary
 
 A: application to vector
+F: boolean false
+T: boolean true
 
 a: application
 b: binder
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rdrop_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rdrop_5.ma
new file mode 100644
index 000000000..70d59f931
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rdrop_5.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 s , break term 46 d , break term 46 e ] break term 46 L1 ≡ break term 46 L2 )"
+   non associative with precedence 45
+   for @{ 'RDrop $s $d $e $L1 $L2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rdropstar_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rdropstar_4.ma
new file mode 100644
index 000000000..94906922f
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rdropstar_4.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 s , break term 46 e ] break term 46 L1 ≡ break term 46 L2 )"
+   non associative with precedence 45
+   for @{ 'RDropStar $s $e $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 05b77349e..798b6eb79 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma
@@ -25,7 +25,7 @@ include "basic_2/relocation/lsuby.ma".
 inductive cpy: ynat → ynat → relation4 genv lenv term term ≝
 | cpy_atom : ∀I,G,L,d,e. cpy d e G L (⓪{I}) (⓪{I})
 | cpy_subst: ∀I,G,L,K,V,W,i,d,e. d ≤ yinj i → i < d+e →
-             ⇩[0, i] L ≡ K.ⓑ{I}V → ⇧[0, i+1] V ≡ W → cpy d e G L (#i) W
+             ⇩[i] L ≡ K.ⓑ{I}V → ⇧[0, i+1] V ≡ W → cpy d e G L (#i) W
 | cpy_bind : ∀a,I,G,L,V1,V2,T1,T2,d,e.
              cpy d e G L V1 V2 → cpy (⫯d) e G (L.ⓑ{I}V2) T1 T2 →
              cpy d e G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
@@ -39,7 +39,7 @@ interpretation "context-sensitive extended ordinary substritution (term)"
 
 (* Basic properties *********************************************************)
 
-lemma lsuby_cpy_trans: ∀G,d,e. lsub_trans … (cpy d e G) (lsuby d e). 
+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
@@ -53,7 +53,7 @@ lemma cpy_refl: ∀G,T,L,d,e. ⦃G, L⦄ ⊢ T ▶×[d, e] T.
 #G #T elim T -T // * /2 width=1 by cpy_bind, cpy_flat/
 qed.
 
-lemma cpy_full: ∀I,G,K,V,T1,L,d. ⇩[0, d] L ≡ K.ⓑ{I}V →
+lemma cpy_full: ∀I,G,K,V,T1,L,d. ⇩[d] L ≡ K.ⓑ{I}V →
                 ∃∃T2,T. ⦃G, L⦄ ⊢ T1 ▶×[d, 1] T2 & ⇧[d, 1] T ≡ T2.
 #I #G #K #V #T1 elim T1 -T1
 [ * #i #L #d #HLK
@@ -67,7 +67,7 @@ lemma cpy_full: ∀I,G,K,V,T1,L,d. ⇩[0, d] L ≡ K.ⓑ{I}V →
 | * [ #a ] #J #W1 #U1 #IHW1 #IHU1 #L #d #HLK
   elim (IHW1 … HLK) -IHW1 #W2 #W #HW12 #HW2
   [ elim (IHU1 (L.ⓑ{J}W2) (d+1)) -IHU1
-    /3 width=9 by cpy_bind, ldrop_ldrop, lift_bind, ex2_2_intro/
+    /3 width=9 by cpy_bind, ldrop_drop, lift_bind, ex2_2_intro/
   | elim (IHU1 … HLK) -IHU1 -HLK
     /3 width=8 by cpy_flat, lift_flat, ex2_2_intro/
   ]
@@ -186,7 +186,7 @@ qed-.
 fact cpy_inv_atom1_aux: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶×[d, e] T2 → ∀J. T1 = ⓪{J} →
                         T2 = ⓪{J} ∨
                         ∃∃I,K,V,i. d ≤ yinj i & i < d + e &
-                                   ⇩[O, i] L ≡ K.ⓑ{I}V &
+                                   ⇩[i] L ≡ K.ⓑ{I}V &
                                    ⇧[O, i+1] V ≡ T2 &
                                    J = LRef i.
 #G #L #T1 #T2 #d #e * -G -L -T1 -T2 -d -e
@@ -200,7 +200,7 @@ qed-.
 lemma cpy_inv_atom1: ∀I,G,L,T2,d,e. ⦃G, L⦄ ⊢ ⓪{I} ▶×[d, e] T2 →
                      T2 = ⓪{I} ∨
                      ∃∃J,K,V,i. d ≤ yinj i & i < d + e &
-                                ⇩[O, i] L ≡ K.ⓑ{J}V &
+                                ⇩[i] L ≡ K.ⓑ{J}V &
                                 ⇧[O, i+1] V ≡ T2 &
                                 I = LRef i.
 /2 width=4 by cpy_inv_atom1_aux/ qed-.
@@ -214,7 +214,7 @@ qed-.
 lemma cpy_inv_lref1: ∀G,L,T2,i,d,e. ⦃G, L⦄ ⊢ #i ▶×[d, e] T2 →
                      T2 = #i ∨
                      ∃∃I,K,V. d ≤ i & i < d + e &
-                              ⇩[O, i] L ≡ K.ⓑ{I}V &
+                              ⇩[i] L ≡ K.ⓑ{I}V &
                               ⇧[O, i+1] V ≡ T2.
 #G #L #T2 #i #d #e #H
 elim (cpy_inv_atom1 … H) -H /2 width=1 by or_introl/
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 85203f203..38ba768e8 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_lift.ma
@@ -20,13 +20,13 @@ include "basic_2/relocation/cpy.ma".
 (* Properties on relocation *************************************************)
 
 lemma cpy_lift_le: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶×[dt, et] T2 →
-                   ∀L,U1,U2,d,e. ⇩[d, e] L ≡ K →
+                   ∀L,U1,U2,s,d,e. ⇩[s, d, e] L ≡ K →
                    ⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 →
                    dt + et ≤ d → ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2.
 #G #K #T1 #T2 #dt #et #H elim H -G -K -T1 -T2 -dt -et
-[ #I #G #K #dt #et #L #U1 #U2 #d #e #_ #H1 #H2 #_
+[ #I #G #K #dt #et #L #U1 #U2 #s #d #e #_ #H1 #H2 #_
   >(lift_mono … H1 … H2) -H1 -H2 //
-| #I #G #K #KV #V #W #i #dt #et #Hdti #Hidet #HKV #HVW #L #U1 #U2 #d #e #HLK #H #HWU2 #Hdetd
+| #I #G #K #KV #V #W #i #dt #et #Hdti #Hidet #HKV #HVW #L #U1 #U2 #s #d #e #HLK #H #HWU2 #Hdetd
   lapply (ylt_yle_trans … Hdetd … Hidet) -Hdetd #Hid
   lapply (ylt_inv_inj … Hid) -Hid #Hid
   lapply (lift_inv_lref1_lt … H … Hid) -H #H destruct
@@ -34,25 +34,25 @@ lemma cpy_lift_le: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶×[dt, et] T2 →
   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 #_ #HVY
   >(lift_mono … HVY … HVW) -Y -HVW #H destruct /2 width=5 by cpy_subst/
-| #a #I #G #K #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hdetd
+| #a #I #G #K #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #s #d #e #HLK #H1 #H2 #Hdetd
   elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1
   elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct
-  /4 width=6 by cpy_bind, ldrop_skip, yle_succ/
-| #G #I #K #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hdetd
+  /4 width=7 by cpy_bind, ldrop_skip, yle_succ/
+| #G #I #K #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #s #d #e #HLK #H1 #H2 #Hdetd
   elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1
   elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct
-  /3 width=6 by cpy_flat/
+  /3 width=7 by cpy_flat/
 ]
 qed-.
 
 lemma cpy_lift_be: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶×[dt, et] T2 →
-                   ∀L,U1,U2,d,e. ⇩[d, e] L ≡ K →
+                   ∀L,U1,U2,s,d,e. ⇩[s, d, e] L ≡ K →
                    ⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 →
                    dt ≤ d → d ≤ dt + et → ⦃G, L⦄ ⊢ U1 ▶×[dt, et + e] U2.
 #G #K #T1 #T2 #dt #et #H elim H -G -K -T1 -T2 -dt -et
-[ #I #G #K #dt #et #L #U1 #U2 #d #e #_ #H1 #H2 #_ #_
+[ #I #G #K #dt #et #L #U1 #U2 #s #d #e #_ #H1 #H2 #_ #_
   >(lift_mono … H1 … H2) -H1 -H2 //
-| #I #G #K #KV #V #W #i #dt #et #Hdti #Hidet #HKV #HVW #L #U1 #U2 #d #e #HLK #H #HWU2 #Hdtd #_
+| #I #G #K #KV #V #W #i #dt #et #Hdti #Hidet #HKV #HVW #L #U1 #U2 #s #d #e #HLK #H #HWU2 #Hdtd #_
   elim (lift_inv_lref1 … H) -H * #Hid #H destruct
   [ -Hdtd
     lapply (ylt_yle_trans … (dt+et+e) … Hidet) // -Hidet #Hidete
@@ -65,68 +65,68 @@ lemma cpy_lift_be: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶×[dt, et] T2 →
     lapply (transitive_le … Hdtd Hid) -Hdtd #Hdti
     lapply (lift_trans_be … HVW … HWU2 ? ?) -W /2 width=1 by le_S/ >plus_plus_comm_23 #HVU2
     lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K // -Hid
-    /4 width=5 by cpy_subst, monotonic_ylt_plus_dx, yle_plus_dx1_trans, yle_inj/
+    /4 width=5 by cpy_subst, ldrop_inv_gen, monotonic_ylt_plus_dx, yle_plus_dx1_trans, yle_inj/
   ]
-| #a #I #G #K #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hdtd #Hddet
+| #a #I #G #K #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #s #d #e #HLK #H1 #H2 #Hdtd #Hddet
   elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1
   elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct
-  /4 width=6 by cpy_bind, ldrop_skip, yle_succ/
-| #I #G #K #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hdetd
+  /4 width=7 by cpy_bind, ldrop_skip, yle_succ/
+| #I #G #K #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #s #d #e #HLK #H1 #H2 #Hdetd
   elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1
   elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct
-  /3 width=6 by cpy_flat/
+  /3 width=7 by cpy_flat/
 ]
 qed-.
 
 lemma cpy_lift_ge: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶×[dt, et] T2 →
-                   ∀L,U1,U2,d,e. ⇩[d, e] L ≡ K →
+                   ∀L,U1,U2,s,d,e. ⇩[s, d, e] L ≡ K →
                    ⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 →
                    d ≤ dt → ⦃G, L⦄ ⊢ U1 ▶×[dt+e, et] U2.
 #G #K #T1 #T2 #dt #et #H elim H -G -K -T1 -T2 -dt -et
-[ #I #G #K #dt #et #L #U1 #U2 #d #e #_ #H1 #H2 #_
+[ #I #G #K #dt #et #L #U1 #U2 #s #d #e #_ #H1 #H2 #_
   >(lift_mono … H1 … H2) -H1 -H2 //
-| #I #G #K #KV #V #W #i #dt #et #Hdti #Hidet #HKV #HVW #L #U1 #U2 #d #e #HLK #H #HWU2 #Hddt
+| #I #G #K #KV #V #W #i #dt #et #Hdti #Hidet #HKV #HVW #L #U1 #U2 #s #d #e #HLK #H #HWU2 #Hddt
   lapply (yle_trans … Hddt … Hdti) -Hddt #Hid
   elim (yle_inv_inj2 … Hid) -Hid #dd #Hddi #H0 destruct
   lapply (lift_inv_lref1_ge … H … Hddi) -H #H destruct
   lapply (lift_trans_be … HVW … HWU2 ? ?) -W /2 width=1 by le_S/ >plus_plus_comm_23 #HVU2
   lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K // -Hddi
-  /3 width=5 by cpy_subst, monotonic_ylt_plus_dx, monotonic_yle_plus_dx/
-| #a #I #G #K #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hddt
+  /3 width=5 by cpy_subst, ldrop_inv_gen, monotonic_ylt_plus_dx, monotonic_yle_plus_dx/
+| #a #I #G #K #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #s #d #e #HLK #H1 #H2 #Hddt
   elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1
   elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct
-  /4 width=5 by cpy_bind, ldrop_skip, yle_succ/
-| #I #G #K #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hddt
+  /4 width=6 by cpy_bind, ldrop_skip, yle_succ/
+| #I #G #K #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #s #d #e #HLK #H1 #H2 #Hddt
   elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1
   elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct
-  /3 width=5 by cpy_flat/
+  /3 width=6 by cpy_flat/
 ]
 qed-.
 
 (* Inversion lemmas on relocation *******************************************)
 
 lemma cpy_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 →
+                        ∀K,s,d,e. ⇩[s, 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 elim H -G -L -U1 -U2 -dt -et
-[ * #i #G #L #dt #et #K #d #e #_ #T1 #H #_
+[ * #i #G #L #dt #et #K #s #d #e #_ #T1 #H #_
   [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by ex2_intro/
   | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by lift_lref_ge_minus, lift_lref_lt, ex2_intro/
   | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by ex2_intro/
   ]
-| #I #G #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #d #e #HLK #T1 #H #Hdetd
+| #I #G #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #s #d #e #HLK #T1 #H #Hdetd
   lapply (ylt_yle_trans … Hdetd … Hidet) -Hdetd #Hid
   lapply (ylt_inv_inj … Hid) -Hid #Hid
   lapply (lift_inv_lref2_lt … H … Hid) -H #H destruct
   elim (ldrop_conf_lt … HLK … HLKV) -L // #L #U #HKL #_ #HUV
   elim (lift_trans_le … HUV … HVW) -V // >minus_plus <plus_minus_m_m // -Hid /3 width=5 by cpy_subst, ex2_intro/
-| #a #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #d #e #HLK #X #H #Hdetd
+| #a #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #s #d #e #HLK #X #H #Hdetd
   elim (lift_inv_bind2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct
   elim (IHW12 … HLK … HVW1) -W1 // #V2 #HV12 #HVW2
   elim (IHU12 … HTU1) -IHU12 -HTU1
-  /3 width=5 by cpy_bind, yle_succ, ldrop_skip, lift_bind, ex2_intro/
-| #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #d #e #HLK #X #H #Hdetd
+  /3 width=6 by cpy_bind, yle_succ, ldrop_skip, lift_bind, ex2_intro/
+| #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #s #d #e #HLK #X #H #Hdetd
   elim (lift_inv_flat2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct
   elim (IHW12 … HLK … HVW1) -W1 //
   elim (IHU12 … HLK … HTU1) -U1 -HLK
@@ -135,16 +135,16 @@ lemma cpy_inv_lift1_le: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 
 qed-.
 
 lemma cpy_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 →
+                        ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
+                        dt ≤ d → yinj d + e ≤ dt + et →
                         ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶×[dt, et-e] T2 & ⇧[d, e] T2 ≡ U2.
 #G #L #U1 #U2 #dt #et #H elim H -G -L -U1 -U2 -dt -et
-[ * #i #G #L #dt #et #K #d #e #_ #T1 #H #_ #_
+[ * #i #G #L #dt #et #K #s #d #e #_ #T1 #H #_ #_
   [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by ex2_intro/
   | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by lift_lref_ge_minus, lift_lref_lt, ex2_intro/
   | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by ex2_intro/
   ]
-| #I #G #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #d #e #HLK #T1 #H #Hdtd #Hdedet
+| #I #G #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #s #d #e #HLK #T1 #H #Hdtd #Hdedet
   lapply (yle_fwd_plus_ge_inj … Hdtd Hdedet) #Heet
   elim (lift_inv_lref2 … H) -H * #Hid #H destruct [ -Hdtd -Hidet | -Hdti -Hdedet ]
   [ lapply (ylt_yle_trans i d (dt+(et-e)) ? ?) /2 width=1 by ylt_inj/
@@ -160,12 +160,12 @@ lemma cpy_inv_lift1_be: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 
     @(ex2_intro … H) @(cpy_subst … HKV HV1) // (**) (* explicit constructor *)
     >yplus_minus_assoc_inj /3 width=1 by monotonic_ylt_minus_dx, yle_inj/
   ]
-| #a #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #d #e #HLK #X #H #Hdtd #Hdedet
+| #a #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #s #d #e #HLK #X #H #Hdtd #Hdedet
   elim (lift_inv_bind2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct
   elim (IHW12 … HLK … HVW1) -W1 // #V2 #HV12 #HVW2
   elim (IHU12 … HTU1) -U1
-  /3 width=5 by cpy_bind, ldrop_skip, lift_bind, yle_succ, ex2_intro/
-| #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #d #e #HLK #X #H #Hdtd #Hdedet
+  /3 width=6 by cpy_bind, ldrop_skip, lift_bind, yle_succ, ex2_intro/
+| #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #s #d #e #HLK #X #H #Hdtd #Hdedet
   elim (lift_inv_flat2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct
   elim (IHW12 … HLK … HVW1) -W1 //
   elim (IHU12 … HLK … HTU1) -U1 -HLK //
@@ -174,16 +174,16 @@ lemma cpy_inv_lift1_be: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 
 qed-.
 
 lemma cpy_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 →
+                        ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
+                        yinj d + e ≤ dt →
                         ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶×[dt-e, et] T2 & ⇧[d, e] T2 ≡ U2.
 #G #L #U1 #U2 #dt #et #H elim H -G -L -U1 -U2 -dt -et
-[ * #i #G #L #dt #et #K #d #e #_ #T1 #H #_
+[ * #i #G #L #dt #et #K #s #d #e #_ #T1 #H #_
   [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by ex2_intro/
   | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by lift_lref_ge_minus, lift_lref_lt, ex2_intro/
   | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by ex2_intro/
   ]
-| #I #G #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #d #e #HLK #T1 #H #Hdedt
+| #I #G #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #s #d #e #HLK #T1 #H #Hdedt
   lapply (yle_trans … Hdedt … Hdti) #Hdei
   elim (yle_inv_plus_inj2 … Hdedt) -Hdedt #_ #Hedt
   elim (yle_inv_plus_inj2 … Hdei) #Hdie #Hei
@@ -195,13 +195,13 @@ lemma cpy_inv_lift1_ge: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 
   [ /2 width=1 by monotonic_yle_minus_dx/
   | <yplus_minus_comm_inj /2 width=1 by monotonic_ylt_minus_dx/
   ]
-| #a #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #d #e #HLK #X #H #Hdetd
+| #a #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #s #d #e #HLK #X #H #Hdetd
   elim (lift_inv_bind2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct
   elim (yle_inv_plus_inj2 … Hdetd) #_ #Hedt
   elim (IHW12 … HLK … HVW1) -W1 // #V2 #HV12 #HVW2
-  elim (IHU12 … HTU1) -U1 [4: @ldrop_skip // |2: skip |3: /2 width=1 by yle_succ/ ]
+  elim (IHU12 … HTU1) -U1 [4: @ldrop_skip // |2,5: skip |3: /2 width=1 by yle_succ/ ]
   >yminus_succ1_inj /3 width=5 by cpy_bind, lift_bind, ex2_intro/
-| #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #d #e #HLK #X #H #Hdetd
+| #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #s #d #e #HLK #X #H #Hdetd
   elim (lift_inv_flat2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct
   elim (IHW12 … HLK … HVW1) -W1 //
   elim (IHU12 … HLK … HTU1) -U1 -HLK /3 width=5 by cpy_flat, lift_flat, ex2_intro/
@@ -211,10 +211,10 @@ qed-.
 (* Advancd inversion lemmas on relocation ***********************************)
 
 lemma cpy_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 #HU12 #K #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet
+                           ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
+                           d ≤ dt → dt ≤ yinj d + e → yinj d + e ≤ dt + et →
+                           ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶×[d, dt + et - (yinj d + e)] T2 & ⇧[d, e] T2 ≡ U2.
+#G #L #U1 #U2 #dt #et #HU12 #K #s #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet
 elim (cpy_split_up … HU12 (d + e)) -HU12 // -Hdedet #U #HU1 #HU2
 lapply (cpy_weak … HU1 d e ? ?) -HU1 // [ >ymax_pre_sn_comm // ] -Hddt -Hdtde #HU1
 lapply (cpy_inv_lift1_eq … HTU1 … HU1) -HU1 #HU1 destruct
@@ -222,20 +222,20 @@ elim (cpy_inv_lift1_ge … HU2 … HLK … HTU1) -U -L /2 width=3 by ex2_intro/
 qed-.
 
 lemma cpy_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 →
+                           ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
+                           dt ≤ d → dt + et ≤ yinj d + e →
                            ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶×[dt, d-dt] T2 & ⇧[d, e] T2 ≡ U2.
-#G #L #U1 #U2 #dt #et #HU12 #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdetde
+#G #L #U1 #U2 #dt #et #HU12 #K #s #d #e #HLK #T1 #HTU1 #Hdtd #Hdetde
 lapply (cpy_weak … HU12 dt (d+e-dt) ? ?) -HU12 //
 [ >ymax_pre_sn_comm /2 width=1 by yle_plus_dx1_trans/ ] -Hdetde #HU12
 elim (cpy_inv_lift1_be … HU12 … HLK … HTU1) -U1 -L /2 width=3 by ex2_intro/
 qed-.
 
 lemma cpy_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 →
+                           ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
+                           dt ≤ d → d ≤ dt + et → dt + et ≤ yinj d + e →
                            ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶×[dt, d - dt] T2 & ⇧[d, e] T2 ≡ U2.
-#G #L #U1 #U2 #dt #et #HU12 #K #d #e #HLK #T1 #HTU1 #Hdtd #Hddet #Hdetde
+#G #L #U1 #U2 #dt #et #HU12 #K #s #d #e #HLK #T1 #HTU1 #Hdtd #Hddet #Hdetde
 elim (cpy_split_up … HU12 d) -HU12 // #U #HU1 #HU2
 elim (cpy_inv_lift1_le … HU1 … HLK … HTU1) -U1
 [2: >ymax_pre_sn_comm // ] -Hdtd #T #HT1 #HTU
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fqu.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fqu.ma
index 2058b25b7..46f274def 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fqu.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/fqu.ma
@@ -25,7 +25,7 @@ inductive fqu: tri_relation genv lenv term ≝
 | fqu_bind_dx: ∀a,I,G,L,V,T. fqu G L (ⓑ{a,I}V.T) G (L.ⓑ{I}V) T
 | fqu_flat_dx: ∀I,G,L,V,T. fqu G L (ⓕ{I}V.T) G L T
 | fqu_drop   : ∀G,L,K,T,U,e.
-               ⇩[0, e+1] L ≡ K → ⇧[0, e+1] T ≡ U → fqu G L U G K T
+               ⇩[e+1] L ≡ K → ⇧[0, e+1] T ≡ U → fqu G L U G K T
 .
 
 interpretation
@@ -35,12 +35,12 @@ interpretation
 (* Basic properties *********************************************************)
 
 lemma fqu_drop_lt: ∀G,L,K,T,U,e. 0 < e →
-                   ⇩[0, e] L ≡ K → ⇧[0, e] T ≡ U → ⦃G, L, U⦄ ⊃ ⦃G, K, T⦄.
+                   ⇩[e] L ≡ K → ⇧[0, e] T ≡ U → ⦃G, L, U⦄ ⊃ ⦃G, K, T⦄.
 #G #L #K #T #U #e #He >(plus_minus_m_m e 1) /2 width=3 by fqu_drop/
 qed.
 
 lemma fqu_lref_S_lt: ∀I,G,L,V,i. 0 < i → ⦃G, L.ⓑ{I}V, #i⦄ ⊃ ⦃G, L, #(i-1)⦄.
-/3 width=3 by fqu_drop, ldrop_ldrop, lift_lref_ge_minus/
+/3 width=3 by fqu_drop, ldrop_drop, lift_lref_ge_minus/
 qed.
 
 (* Basic forward lemmas *****************************************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq.ma
index de000da70..6601cb963 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq.ma
@@ -24,7 +24,7 @@ inductive fquq: tri_relation genv lenv term ≝
 | fquq_bind_dx: ∀a,I,G,L,V,T. fquq G L (ⓑ{a,I}V.T) G (L.ⓑ{I}V) T
 | fquq_flat_dx: ∀I,G, L,V,T. fquq G L (ⓕ{I}V.T) G L T
 | fquq_drop   : ∀G,L,K,T,U,e.
-                ⇩[0, e] L ≡ K → ⇧[0, e] T ≡ U → fquq G L U G K T
+                ⇩[e] L ≡ K → ⇧[0, e] T ≡ U → fquq G L U G K T
 .
 
 interpretation
@@ -37,7 +37,7 @@ lemma fquq_refl: tri_reflexive … fquq.
 /2 width=3 by fquq_drop/ qed.
 
 lemma fqu_fquq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄.
-#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 // /2 width=3 by fquq_drop/
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 /2 width=3 by fquq_drop/
 qed.
 
 (* Basic forward lemmas *****************************************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_alt.ma
index 1d770dcc4..033959bea 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_alt.ma
@@ -30,7 +30,7 @@ lemma fquqa_refl: tri_reflexive … fquqa.
 // qed.
 
 lemma fquqa_drop: ∀G,L,K,T,U,e.
-                  ⇩[0, e] L ≡ K → ⇧[0, e] T ≡ U → ⦃G, L, U⦄ ⊃⊃⸮ ⦃G, K, T⦄.
+                  ⇩[e] L ≡ K → ⇧[0, e] T ≡ U → ⦃G, L, U⦄ ⊃⊃⸮ ⦃G, K, T⦄.
 #G #L #K #T #U #e #HLK #HTU elim (eq_or_gt e)
 /3 width=5 by fqu_drop_lt, or_introl/ #H destruct
 >(ldrop_inv_O2 … HLK) -L >(lift_inv_O2 … HTU) -T //
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
index ee4780d88..b26b7e95b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
@@ -12,8 +12,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground_2/lib/bool.ma".
 include "ground_2/lib/lstar.ma".
+include "basic_2/notation/relations/rdrop_5.ma".
 include "basic_2/notation/relations/rdrop_4.ma".
+include "basic_2/notation/relations/rdrop_3.ma".
 include "basic_2/grammar/lenv_length.ma".
 include "basic_2/grammar/cl_restricted_weight.ma".
 include "basic_2/relocation/lift.ma".
@@ -21,283 +24,307 @@ include "basic_2/relocation/lift.ma".
 (* BASIC SLICING FOR LOCAL ENVIRONMENTS *************************************)
 
 (* Basic_1: includes: drop_skip_bind *)
-inductive ldrop: relation4 nat nat lenv lenv ≝
-| ldrop_atom : ∀d. ldrop d 0 (⋆) (⋆)
-| ldrop_pair : ∀L,I,V. ldrop 0 0 (L. ⓑ{I} V) (L. ⓑ{I} V)
-| ldrop_ldrop: ∀L1,L2,I,V,e. ldrop 0 e L1 L2 → ldrop 0 (e + 1) (L1. ⓑ{I} V) L2
-| ldrop_skip : ∀L1,L2,I,V1,V2,d,e.
-               ldrop d e L1 L2 → ⇧[d,e] V2 ≡ V1 →
-               ldrop (d + 1) e (L1. ⓑ{I} V1) (L2. ⓑ{I} V2)
+inductive ldrop (s:bool): relation4 nat nat lenv lenv ≝
+| ldrop_atom: ∀d,e. (s = Ⓕ → e = 0) → ldrop s d e (⋆) (⋆)
+| ldrop_pair: ∀I,L,V. ldrop s 0 0 (L.ⓑ{I}V) (L.ⓑ{I}V)
+| ldrop_drop: ∀I,L1,L2,V,e. ldrop s 0 e L1 L2 → ldrop s 0 (e+1) (L1.ⓑ{I}V) L2
+| ldrop_skip: ∀I,L1,L2,V1,V2,d,e.
+              ldrop s d e L1 L2 → ⇧[d, e] V2 ≡ V1 →
+              ldrop s (d+1) e (L1.ⓑ{I}V1) (L2.ⓑ{I}V2)
 .
 
 interpretation
-   "basic slicing (local environment)"
-   'RDrop d e L1 L2 = (ldrop d e L1 L2).
+   "basic slicing (local environment) abstract"
+   'RDrop s d e L1 L2 = (ldrop s d e L1 L2).
+
+interpretation
+   "basic slicing (local environment) general"
+   'RDrop d e L1 L2 = (ldrop true d e L1 L2).
+
+interpretation
+   "basic slicing (local environment) lget"
+   'RDrop e L1 L2 = (ldrop false O e L1 L2).
 
 definition l_liftable: predicate (lenv → relation term) ≝
-                       λR. ∀K,T1,T2. R K T1 T2 → ∀L,d,e. ⇩[d, e] L ≡ K →
+                       λR. ∀K,T1,T2. R K T1 T2 → ∀L,s,d,e. ⇩[s, d, e] L ≡ K →
                        ∀U1. ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 → R L U1 U2.
 
 definition l_deliftable_sn: predicate (lenv → relation term) ≝
-                            λR. ∀L,U1,U2. R L U1 U2 → ∀K,d,e. ⇩[d, e] L ≡ K →
+                            λR. ∀L,U1,U2. R L U1 U2 → ∀K,s,d,e. ⇩[s, d, e] L ≡ K →
                             ∀T1. ⇧[d, e] T1 ≡ U1 →
                             ∃∃T2. ⇧[d, e] T2 ≡ U2 & R K T1 T2.
 
 definition dropable_sn: predicate (relation lenv) ≝
-                        λR. ∀L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀L2. R L1 L2 →
-                        ∃∃K2. R K1 K2 & ⇩[d, e] L2 ≡ K2.
+                        λR. ∀L1,K1,s,d,e. ⇩[s, d, e] L1 ≡ K1 → ∀L2. R L1 L2 →
+                        ∃∃K2. R K1 K2 & ⇩[s, d, e] L2 ≡ K2.
 
 definition dedropable_sn: predicate (relation lenv) ≝
-                          λR. ∀L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀K2. R K1 K2 →
-                          ∃∃L2. R L1 L2 & ⇩[d, e] L2 ≡ K2.
+                          λR. ∀L1,K1,s,d,e. ⇩[s, d, e] L1 ≡ K1 → ∀K2. R K1 K2 →
+                          ∃∃L2. R L1 L2 & ⇩[s, d, e] L2 ≡ K2.
 
 definition dropable_dx: predicate (relation lenv) ≝
-                        λR. ∀L1,L2. R L1 L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 →
-                        ∃∃K1. ⇩[0, e] L1 ≡ K1 & R K1 K2.
+                        λR. ∀L1,L2. R L1 L2 → ∀K2,s,e. ⇩[s, 0, e] L2 ≡ K2 →
+                        ∃∃K1. ⇩[s, 0, e] L1 ≡ K1 & R K1 K2.
 
 (* Basic inversion lemmas ***************************************************)
 
-fact ldrop_inv_atom1_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → L1 = ⋆ →
-                          L2 = ⋆ ∧ e = 0.
-#d #e #L1 #L2 * -d -e -L1 -L2
-[ /2 width=1 by conj/
-| #L #I #V #H destruct
-| #L1 #L2 #I #V #e #_ #H destruct
-| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H destruct
+fact ldrop_inv_atom1_aux: ∀L1,L2,s,d,e. ⇩[s, d, e] L1 ≡ L2 → L1 = ⋆ →
+                          L2 = ⋆ ∧ (s = Ⓕ → e = 0).
+#L1 #L2 #s #d #e * -L1 -L2 -d -e
+[ /3 width=1 by conj/
+| #I #L #V #H destruct
+| #I #L1 #L2 #V #e #_ #H destruct
+| #I #L1 #L2 #V1 #V2 #d #e #_ #_ #H destruct
 ]
 qed-.
 
 (* Basic_1: was: drop_gen_sort *)
-lemma ldrop_inv_atom1: ∀d,e,L2. ⇩[d, e] ⋆ ≡ L2 → L2 = ⋆ ∧ e = 0.
+lemma ldrop_inv_atom1: ∀L2,s,d,e. ⇩[s, d, e] ⋆ ≡ L2 → L2 = ⋆ ∧ (s = Ⓕ → e = 0).
 /2 width=4 by ldrop_inv_atom1_aux/ qed-.
 
-fact ldrop_inv_O1_pair1_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → d = 0 →
-                             ∀K,I,V. L1 = K. ⓑ{I} V →
-                             (e = 0 ∧ L2 = K. ⓑ{I} V) ∨
-                             (0 < e ∧ ⇩[d, e - 1] K ≡ L2).
-#d #e #L1 #L2 * -d -e -L1 -L2
-[ #d #_ #K #I #V #H destruct
-| #L #I #V #_ #K #J #W #HX destruct /3 width=1 by or_introl, conj/
-| #L1 #L2 #I #V #e #HL12 #_ #K #J #W #H destruct /3 width=1 by or_intror, conj/
-| #L1 #L2 #I #V1 #V2 #d #e #_ #_ >commutative_plus normalize #H destruct
+fact ldrop_inv_O1_pair1_aux: ∀L1,L2,s,d,e. ⇩[s, d, e] L1 ≡ L2 → d = 0 →
+                             ∀K,I,V. L1 = K.ⓑ{I}V →
+                             (e = 0 ∧ L2 = K.ⓑ{I}V) ∨
+                             (0 < e ∧ ⇩[s, d, e-1] K ≡ L2).
+#L1 #L2 #s #d #e * -L1 -L2 -d -e
+[ #d #e #_ #_ #K #J #W #H destruct
+| #I #L #V #_ #K #J #W #HX destruct /3 width=1 by or_introl, conj/
+| #I #L1 #L2 #V #e #HL12 #_ #K #J #W #H destruct /3 width=1 by or_intror, conj/
+| #I #L1 #L2 #V1 #V2 #d #e #_ #_ >commutative_plus normalize #H destruct
 ]
 qed-.
 
-lemma ldrop_inv_O1_pair1: ∀e,K,I,V,L2. ⇩[0, e] K. ⓑ{I} V ≡ L2 →
-                          (e = 0 ∧ L2 = K. ⓑ{I} V) ∨
-                          (0 < e ∧ ⇩[0, e - 1] K ≡ L2).
+lemma ldrop_inv_O1_pair1: ∀I,K,L2,V,s,e. ⇩[s, 0, e] K. ⓑ{I} V ≡ L2 →
+                          (e = 0 ∧ L2 = K.ⓑ{I}V) ∨
+                          (0 < e ∧ ⇩[s, 0, e-1] K ≡ L2).
 /2 width=3 by ldrop_inv_O1_pair1_aux/ qed-.
 
-lemma ldrop_inv_pair1: ∀K,I,V,L2. ⇩[0, 0] K. ⓑ{I} V ≡ L2 → L2 = K. ⓑ{I} V.
-#K #I #V #L2 #H
+lemma ldrop_inv_pair1: ∀I,K,L2,V,s. ⇩[s, 0, 0] K.ⓑ{I}V ≡ L2 → L2 = K.ⓑ{I}V.
+#I #K #L2 #V #s #H
 elim (ldrop_inv_O1_pair1 … H) -H * // #H destruct
 elim (lt_refl_false … H)
 qed-.
 
 (* Basic_1: was: drop_gen_drop *)
-lemma ldrop_inv_ldrop1_lt: ∀e,K,I,V,L2.
-                           ⇩[0, e] K. ⓑ{I} V ≡ L2 → 0 < e → ⇩[0, e - 1] K ≡ L2.
-#e #K #I #V #L2 #H #He
+lemma ldrop_inv_drop1_lt: ∀I,K,L2,V,s,e.
+                          ⇩[s, 0, e] K.ⓑ{I}V ≡ L2 → 0 < e → ⇩[s, 0, e-1] K ≡ L2.
+#I #K #L2 #V #s #e #H #He
 elim (ldrop_inv_O1_pair1 … H) -H * // #H destruct
 elim (lt_refl_false … He)
 qed-.
 
-lemma ldrop_inv_ldrop1: ∀e,K,I,V,L2.
-                        ⇩[0, e+1] K. ⓑ{I} V ≡ L2 → ⇩[0, e] K ≡ L2.
-#e #K #I #V #L2 #H lapply (ldrop_inv_ldrop1_lt … H ?) -H //
+lemma ldrop_inv_drop1: ∀I,K,L2,V,s,e.
+                       ⇩[s, 0, e+1] K.ⓑ{I}V ≡ L2 → ⇩[s, 0, e] K ≡ L2.
+#I #K #L2 #V #s #e #H lapply (ldrop_inv_drop1_lt … H ?) -H //
 qed-.
 
-fact ldrop_inv_skip1_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → 0 < d →
-                          ∀I,K1,V1. L1 = K1. ⓑ{I} V1 →
-                          ∃∃K2,V2. ⇩[d - 1, e] K1 ≡ K2 &
-                                   ⇧[d - 1, e] V2 ≡ V1 &
-                                   L2 = K2. ⓑ{I} V2.
-#d #e #L1 #L2 * -d -e -L1 -L2
-[ #d #_ #I #K #V #H destruct
-| #L #I #V #H elim (lt_refl_false … H)
-| #L1 #L2 #I #V #e #_ #H elim (lt_refl_false … H)
-| #X #L2 #Y #Z #V2 #d #e #HL12 #HV12 #_ #I #L1 #V1 #H destruct /2 width=5 by ex3_2_intro/
+fact ldrop_inv_skip1_aux: ∀L1,L2,s,d,e. ⇩[s, d, e] L1 ≡ L2 → 0 < d →
+                          ∀I,K1,V1. L1 = K1.ⓑ{I}V1 →
+                          ∃∃K2,V2. ⇩[s, d-1, e] K1 ≡ K2 &
+                                   ⇧[d-1, e] V2 ≡ V1 &
+                                   L2 = K2.ⓑ{I}V2.
+#L1 #L2 #s #d #e * -L1 -L2 -d -e
+[ #d #e #_ #_ #J #K1 #W1 #H destruct
+| #I #L #V #H elim (lt_refl_false … H)
+| #I #L1 #L2 #V #e #_ #H elim (lt_refl_false … H)
+| #I #L1 #L2 #V1 #V2 #d #e #HL12 #HV21 #_ #J #K1 #W1 #H destruct /2 width=5 by ex3_2_intro/
 ]
 qed-.
 
 (* Basic_1: was: drop_gen_skip_l *)
-lemma ldrop_inv_skip1: ∀d,e,I,K1,V1,L2. ⇩[d, e] K1. ⓑ{I} V1 ≡ L2 → 0 < d →
-                       ∃∃K2,V2. ⇩[d - 1, e] K1 ≡ K2 &
-                                ⇧[d - 1, e] V2 ≡ V1 &
-                                L2 = K2. ⓑ{I} V2.
+lemma ldrop_inv_skip1: ∀I,K1,V1,L2,s,d,e. ⇩[s, d, e] K1.ⓑ{I}V1 ≡ L2 → 0 < d →
+                       ∃∃K2,V2. ⇩[s, d-1, e] K1 ≡ K2 &
+                                ⇧[d-1, e] V2 ≡ V1 &
+                                L2 = K2.ⓑ{I}V2.
 /2 width=3 by ldrop_inv_skip1_aux/ qed-.
 
-lemma ldrop_inv_O1_pair2: ∀I,K,V,e,L1. ⇩[0, e] L1 ≡ K. ⓑ{I} V →
-                          (e = 0 ∧ L1 = K. ⓑ{I} V) ∨
-                          ∃∃I1,K1,V1. ⇩[0, e - 1] K1 ≡ K. ⓑ{I} V & L1 = K1.ⓑ{I1}V1 & 0 < e.
-#I #K #V #e *
+lemma ldrop_inv_O1_pair2: ∀I,K,V,s,e,L1. ⇩[s, 0, e] L1 ≡ K.ⓑ{I}V →
+                          (e = 0 ∧ L1 = K.ⓑ{I}V) ∨
+                          ∃∃I1,K1,V1. ⇩[s, 0, e-1] K1 ≡ K.ⓑ{I}V & L1 = K1.ⓑ{I1}V1 & 0 < e.
+#I #K #V #s #e *
 [ #H elim (ldrop_inv_atom1 … H) -H #H destruct
 | #L1 #I1 #V1 #H
   elim (ldrop_inv_O1_pair1 … H) -H *
   [ #H1 #H2 destruct /3 width=1 by or_introl, conj/
-  | /3 width=5/
+  | /3 width=5 by ex3_3_intro, or_intror/
   ]
 ]
 qed-.
 
-fact ldrop_inv_skip2_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → 0 < d →
-                          ∀I,K2,V2. L2 = K2. ⓑ{I} V2 →
-                          ∃∃K1,V1. ⇩[d - 1, e] K1 ≡ K2 &
-                                   ⇧[d - 1, e] V2 ≡ V1 &
-                                   L1 = K1. ⓑ{I} V1.
-#d #e #L1 #L2 * -d -e -L1 -L2
-[ #d #_ #I #K #V #H destruct
-| #L #I #V #H elim (lt_refl_false … H)
-| #L1 #L2 #I #V #e #_ #H elim (lt_refl_false … H)
-| #L1 #X #Y #V1 #Z #d #e #HL12 #HV12 #_ #I #L2 #V2 #H destruct /2 width=5 by ex3_2_intro/
+fact ldrop_inv_skip2_aux: ∀L1,L2,s,d,e. ⇩[s, d, e] L1 ≡ L2 → 0 < d →
+                          ∀I,K2,V2. L2 = K2.ⓑ{I}V2 →
+                          ∃∃K1,V1. ⇩[s, d-1, e] K1 ≡ K2 &
+                                   ⇧[d-1, e] V2 ≡ V1 &
+                                   L1 = K1.ⓑ{I}V1.
+#L1 #L2 #s #d #e * -L1 -L2 -d -e
+[ #d #e #_ #_ #J #K2 #W2 #H destruct
+| #I #L #V #H elim (lt_refl_false … H)
+| #I #L1 #L2 #V #e #_ #H elim (lt_refl_false … H)
+| #I #L1 #L2 #V1 #V2 #d #e #HL12 #HV21 #_ #J #K2 #W2 #H destruct /2 width=5 by ex3_2_intro/
 ]
 qed-.
 
 (* Basic_1: was: drop_gen_skip_r *)
-lemma ldrop_inv_skip2: ∀d,e,I,L1,K2,V2. ⇩[d, e] L1 ≡ K2. ⓑ{I} V2 → 0 < d →
-                       ∃∃K1,V1. ⇩[d - 1, e] K1 ≡ K2 & ⇧[d - 1, e] V2 ≡ V1 &
-                                L1 = K1. ⓑ{I} V1.
+lemma ldrop_inv_skip2: ∀I,L1,K2,V2,s,d,e. ⇩[s, d, e] L1 ≡ K2.ⓑ{I}V2 → 0 < d →
+                       ∃∃K1,V1. ⇩[s, d-1, e] K1 ≡ K2 & ⇧[d-1, e] V2 ≡ V1 &
+                                L1 = K1.ⓑ{I}V1.
 /2 width=3 by ldrop_inv_skip2_aux/ qed-.
 
 (* Basic properties *********************************************************)
 
+lemma ldrop_refl_atom_O2: ∀s,d. ⇩[s, d, O] ⋆ ≡ ⋆.
+/2 width=1 by ldrop_atom/ qed.
+
 (* Basic_1: was by definition: drop_refl *)
-lemma ldrop_refl: ∀L,d. ⇩[d, 0] L ≡ L.
+lemma ldrop_refl: ∀L,d,s. ⇩[s, d, 0] L ≡ L.
 #L elim L -L //
-#L #I #V #IHL #d @(nat_ind_plus … d) -d /2 width=1 by ldrop_pair, ldrop_skip/
+#L #I #V #IHL #d #s @(nat_ind_plus … d) -d /2 width=1 by ldrop_pair, ldrop_skip/
 qed.
 
-lemma ldrop_ldrop_lt: ∀L1,L2,I,V,e.
-                      ⇩[0, e - 1] L1 ≡ L2 → 0 < e → ⇩[0, e] L1. ⓑ{I} V ≡ L2.
-#L1 #L2 #I #V #e #HL12 #He >(plus_minus_m_m e 1) /2 width=1 by ldrop_ldrop/
+lemma ldrop_drop_lt: ∀I,L1,L2,V,s,e.
+                     ⇩[s, 0, e-1] L1 ≡ L2 → 0 < e → ⇩[s, 0, e] L1.ⓑ{I}V ≡ L2.
+#I #L1 #L2 #V #s #e #HL12 #He >(plus_minus_m_m e 1) /2 width=1 by ldrop_drop/
 qed.
 
-lemma ldrop_skip_lt: ∀L1,L2,I,V1,V2,d,e.
-                     ⇩[d - 1, e] L1 ≡ L2 → ⇧[d - 1, e] V2 ≡ V1 → 0 < d →
-                     ⇩[d, e] L1. ⓑ{I} V1 ≡ L2. ⓑ{I} V2.
-#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV21 #Hd >(plus_minus_m_m d 1) /2 width=1 by ldrop_skip/
+lemma ldrop_skip_lt: ∀I,L1,L2,V1,V2,s,d,e.
+                     ⇩[s, d-1, e] L1 ≡ L2 → ⇧[d-1, e] V2 ≡ V1 → 0 < d →
+                     ⇩[s, d, e] L1. ⓑ{I} V1 ≡ L2.ⓑ{I}V2.
+#I #L1 #L2 #V1 #V2 #s #d #e #HL12 #HV21 #Hd >(plus_minus_m_m d 1) /2 width=1 by ldrop_skip/
 qed.
 
-lemma ldrop_O1_le: ∀e,L. e ≤ |L| → ∃K. ⇩[0, e] L ≡ K.
-#e @(nat_ind_plus … e) -e /2 width=2/
+lemma ldrop_O1_le: ∀e,L. e ≤ |L| → ∃K. ⇩[e] L ≡ K.
+#e @(nat_ind_plus … e) -e /2 width=2 by ex_intro/
 #e #IHe *
 [ #H lapply (le_n_O_to_eq … H) -H >commutative_plus normalize #H destruct
 | #L #I #V normalize #H
-  elim (IHe L) -IHe /2 width=1/ -H /3 width=2 by ldrop_ldrop, ex_intro/
+  elim (IHe L) -IHe /3 width=2 by ldrop_drop, monotonic_pred, ex_intro/
 ]
-qed.
+qed-.
 
-lemma ldrop_O1_lt: ∀L,e. e < |L| → ∃∃I,K,V. ⇩[0, e] L ≡ K.ⓑ{I}V.
+lemma ldrop_O1_lt: ∀L,e. e < |L| → ∃∃I,K,V. ⇩[e] L ≡ K.ⓑ{I}V.
 #L elim L -L
 [ #e #H elim (lt_zero_false … H)
 | #L #I #V #IHL #e @(nat_ind_plus … e) -e /2 width=4 by ldrop_pair, ex1_3_intro/
   #e #_ normalize #H
-  elim (IHL e) -IHL /3 width=4 by ldrop_ldrop, lt_plus_to_minus_r, lt_plus_to_lt_l, ex1_3_intro/
+  elim (IHL e) -IHL /3 width=4 by ldrop_drop, lt_plus_to_minus_r, lt_plus_to_lt_l, ex1_3_intro/
 ]
+qed-.
+
+lemma ldrop_FT: ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ L2 → ⇩[Ⓣ, d, e] L1 ≡ L2.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
+/3 width=1 by ldrop_atom, ldrop_drop, ldrop_skip/
 qed.
 
+lemma ldrop_gen: ∀L1,L2,s,d,e. ⇩[Ⓕ, d, e] L1 ≡ L2 → ⇩[s, d, e] L1 ≡ L2.
+#L1 #L2 * /2 width=1 by ldrop_FT/
+qed-.
+
+lemma ldrop_T: ∀L1,L2,s,d,e. ⇩[s, d, e] L1 ≡ L2 → ⇩[Ⓣ, d, e] L1 ≡ L2.
+#L1 #L2 * /2 width=1 by ldrop_FT/
+qed-.
+
 lemma l_liftable_LTC: ∀R. l_liftable R → l_liftable (LTC … R).
 #R #HR #K #T1 #T2 #H elim H -T2
-[ /3 width=9/
-| #T #T2 #_ #HT2 #IHT1 #L #d #e #HLK #U1 #HTU1 #U2 #HTU2
-  elim (lift_total T d e) /4 width=11 by step/
+[ /3 width=10 by inj/
+| #T #T2 #_ #HT2 #IHT1 #L #s #d #e #HLK #U1 #HTU1 #U2 #HTU2
+  elim (lift_total T d e) /4 width=12 by step/
 ]
-qed.
+qed-.
 
 lemma l_deliftable_sn_LTC: ∀R. l_deliftable_sn R → l_deliftable_sn (LTC … R).
 #R #HR #L #U1 #U2 #H elim H -U2
-[ #U2 #HU12 #K #d #e #HLK #T1 #HTU1
+[ #U2 #HU12 #K #s #d #e #HLK #T1 #HTU1
   elim (HR … HU12 … HLK … HTU1) -HR -L -U1 /3 width=3 by inj, ex2_intro/
-| #U #U2 #_ #HU2 #IHU1 #K #d #e #HLK #T1 #HTU1
+| #U #U2 #_ #HU2 #IHU1 #K #s #d #e #HLK #T1 #HTU1
   elim (IHU1 … HLK … HTU1) -IHU1 -U1 #T #HTU #HT1
   elim (HR … HU2 … HLK … HTU) -HR -L -U /3 width=5 by step, ex2_intro/
 ]
-qed.
+qed-.
 
 lemma dropable_sn_TC: ∀R. dropable_sn R → dropable_sn (TC … R).
-#R #HR #L1 #K1 #d #e #HLK1 #L2 #H elim H -L2
-[ #L2 #HL12
-  elim (HR … HLK1 … HL12) -HR -L1 /3 width=3 by inj, ex2_intro/
-| #L #L2 #_ #HL2 * #K #HK1 #HLK
-  elim (HR … HLK … HL2) -HR -L /3 width=3 by step, ex2_intro/
+#R #HR #L1 #K1 #s #d #e #HLK1 #L2 #H elim H -L2
+[ #L2 #HL12 elim (HR … HLK1 … HL12) -HR -L1
+  /3 width=3 by inj, ex2_intro/
+| #L #L2 #_ #HL2 * #K #HK1 #HLK elim (HR … HLK … HL2) -HR -L
+  /3 width=3 by step, ex2_intro/
 ]
-qed.
+qed-.
 
 lemma dedropable_sn_TC: ∀R. dedropable_sn R → dedropable_sn (TC … R).
-#R #HR #L1 #K1 #d #e #HLK1 #K2 #H elim H -K2
-[ #K2 #HK12
-  elim (HR … HLK1 … HK12) -HR -K1 /3 width=3 by inj, ex2_intro/
-| #K #K2 #_ #HK2 * #L #HL1 #HLK
-  elim (HR … HLK … HK2) -HR -K /3 width=3 by step, ex2_intro/
+#R #HR #L1 #K1 #s #d #e #HLK1 #K2 #H elim H -K2
+[ #K2 #HK12 elim (HR … HLK1 … HK12) -HR -K1
+  /3 width=3 by inj, ex2_intro/
+| #K #K2 #_ #HK2 * #L #HL1 #HLK elim (HR … HLK … HK2) -HR -K
+  /3 width=3 by step, ex2_intro/
 ]
-qed.
+qed-.
 
 lemma dropable_dx_TC: ∀R. dropable_dx R → dropable_dx (TC … R).
 #R #HR #L1 #L2 #H elim H -L2
-[ #L2 #HL12 #K2 #e #HLK2
-  elim (HR … HL12 … HLK2) -HR -L2 /3 width=3 by inj, ex2_intro/
-| #L #L2 #_ #HL2 #IHL1 #K2 #e #HLK2
-  elim (HR … HL2 … HLK2) -HR -L2 #K #HLK #HK2
-  elim (IHL1 … HLK) -L /3 width=5 by step, ex2_intro/
+[ #L2 #HL12 #K2 #s #e #HLK2 elim (HR … HL12 … HLK2) -HR -L2
+  /3 width=3 by inj, ex2_intro/
+| #L #L2 #_ #HL2 #IHL1 #K2 #s #e #HLK2 elim (HR … HL2 … HLK2) -HR -L2
+  #K #HLK #HK2 elim (IHL1 … HLK) -L
+  /3 width=5 by step, ex2_intro/
 ]
-qed.
+qed-.
 
 lemma l_deliftable_sn_llstar: ∀R. l_deliftable_sn R →
                               ∀l. l_deliftable_sn (llstar … R l).
 #R #HR #l #L #U1 #U2 #H @(lstar_ind_r … l U2 H) -l -U2
 [ /2 width=3 by lstar_O, ex2_intro/
-| #l #U #U2 #_ #HU2 #IHU1 #K #d #e #HLK #T1 #HTU1
+| #l #U #U2 #_ #HU2 #IHU1 #K #s #d #e #HLK #T1 #HTU1
   elim (IHU1 … HLK … HTU1) -IHU1 -U1 #T #HTU #HT1
   elim (HR … HU2 … HLK … HTU) -HR -L -U /3 width=5 by lstar_dx, ex2_intro/
 ]
-qed.
+qed-.
 
 (* Basic forvard lemmas *****************************************************)
 
 (* Basic_1: was: drop_S *)
-lemma ldrop_fwd_ldrop2: ∀L1,I2,K2,V2,e. ⇩[O, e] L1 ≡ K2. ⓑ{I2} V2 →
-                        ⇩[O, e + 1] L1 ≡ K2.
+lemma ldrop_fwd_drop2: ∀L1,I2,K2,V2,s,e. ⇩[s, O, e] L1 ≡ K2. ⓑ{I2} V2 →
+                       ⇩[s, O, e + 1] L1 ≡ K2.
 #L1 elim L1 -L1
-[ #I2 #K2 #V2 #e #H lapply (ldrop_inv_atom1 … H) -H * #H destruct
-| #K1 #I1 #V1 #IHL1 #I2 #K2 #V2 #e #H
+[ #I2 #K2 #V2 #s #e #H lapply (ldrop_inv_atom1 … H) -H * #H destruct
+| #K1 #I1 #V1 #IHL1 #I2 #K2 #V2 #s #e #H
   elim (ldrop_inv_O1_pair1 … H) -H * #He #H
-  [ -IHL1 destruct /2 width=1/
-  | @ldrop_ldrop >(plus_minus_m_m e 1) /2 width=3 by /
+  [ -IHL1 destruct /2 width=1 by ldrop_drop/
+  | @ldrop_drop >(plus_minus_m_m e 1) /2 width=3 by/
   ]
 ]
 qed-.
 
-lemma ldrop_fwd_length: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → |L1| = |L2| + e.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize /2 width=1 by /
+lemma ldrop_fwd_length: ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ L2 → |L1| = |L2| + e.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize /2 width=1 by/
 qed-.
 
-lemma ldrop_fwd_length_minus2: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → |L2| = |L1| - e.
+lemma ldrop_fwd_length_minus2: ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ L2 → |L2| = |L1| - e.
 #L1 #L2 #d #e #H lapply (ldrop_fwd_length … H) -H /2 width=1 by plus_minus, le_n/
 qed-.
 
-lemma ldrop_fwd_length_minus4: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → e = |L1| - |L2|.
+lemma ldrop_fwd_length_minus4: ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ L2 → e = |L1| - |L2|.
 #L1 #L2 #d #e #H lapply (ldrop_fwd_length … H) -H //
 qed-.
 
-lemma ldrop_fwd_length_le2: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → e ≤ |L1|.
+lemma ldrop_fwd_length_le2: ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ L2 → e ≤ |L1|.
 #L1 #L2 #d #e #H lapply (ldrop_fwd_length … H) -H //
 qed-.
 
-lemma ldrop_fwd_length_le4: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → |L2| ≤ |L1|.
+lemma ldrop_fwd_length_le4: ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ L2 → |L2| ≤ |L1|.
 #L1 #L2 #d #e #H lapply (ldrop_fwd_length … H) -H //
 qed-.
 
 lemma ldrop_fwd_length_lt2: ∀L1,I2,K2,V2,d,e.
-                            ⇩[d, e] L1 ≡ K2. ⓑ{I2} V2 → e < |L1|.
+                            ⇩[Ⓕ, d, e] L1 ≡ K2. ⓑ{I2} V2 → e < |L1|.
 #L1 #I2 #K2 #V2 #d #e #H
 lapply (ldrop_fwd_length … H) normalize in ⊢ (%→?); -I2 -V2 //
 qed-.
 
-lemma ldrop_fwd_length_lt4: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → 0 < e → |L2| < |L1|.
+lemma ldrop_fwd_length_lt4: ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ L2 → 0 < e → |L2| < |L1|.
 #L1 #L2 #d #e #H lapply (ldrop_fwd_length … H) -H /2 width=1 by lt_minus_to_plus_r/
 qed-.
 
-lemma ldrop_fwd_length_eq1: ∀L1,L2,K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 →
+lemma ldrop_fwd_length_eq1: ∀L1,L2,K1,K2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 →
                             |L1| = |L2| → |K1| = |K2|.
 #L1 #L2 #K1 #K2 #d #e #HLK1 #HLK2 #HL12
 lapply (ldrop_fwd_length … HLK1) -HLK1
@@ -305,60 +332,85 @@ lapply (ldrop_fwd_length … HLK2) -HLK2
 /2 width=2 by injective_plus_r/
 qed-.
 
-lemma ldrop_fwd_length_eq2: ∀L1,L2,K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 →
+lemma ldrop_fwd_length_eq2: ∀L1,L2,K1,K2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 →
                             |K1| = |K2| → |L1| = |L2|.
 #L1 #L2 #K1 #K2 #d #e #HLK1 #HLK2 #HL12
 lapply (ldrop_fwd_length … HLK1) -HLK1
 lapply (ldrop_fwd_length … HLK2) -HLK2 //
 qed-.
 
-lemma ldrop_fwd_lw: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ♯{L2} ≤ ♯{L1}.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize
+lemma ldrop_fwd_lw: ∀L1,L2,s,d,e. ⇩[s, d, e] L1 ≡ L2 → ♯{L2} ≤ ♯{L1}.
+#L1 #L2 #s #d #e #H elim H -L1 -L2 -d -e // normalize
 [ /2 width=3 by transitive_le/
-| #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12
+| #I #L1 #L2 #V1 #V2 #d #e #_ #HV21 #IHL12
   >(lift_fwd_tw … HV21) -HV21 /2 width=1 by monotonic_le_plus_l/
 ]
 qed-.
 
-lemma ldrop_fwd_lw_lt: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → 0 < e → ♯{L2} < ♯{L1}.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e //
-[ #L #I #V #H elim (lt_refl_false … H)
-| #L1 #L2 #I #V #e #HL12 #_ #_
+lemma ldrop_fwd_lw_lt: ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ L2 → 0 < e → ♯{L2} < ♯{L1}.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
+[ #d #e #H >H -H //
+| #I #L #V #H elim (lt_refl_false … H)
+| #I #L1 #L2 #V #e #HL12 #_ #_
   lapply (ldrop_fwd_lw … HL12) -HL12 #HL12
   @(le_to_lt_to_lt … HL12) -HL12 //
-| #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12 #H normalize in ⊢ (?%%); -I
+| #I #L1 #L2 #V1 #V2 #d #e #_ #HV21 #IHL12 #H normalize in ⊢ (?%%); -I
   >(lift_fwd_tw … HV21) -V2 /3 by lt_minus_to_plus/
 ]
 qed-.
 
-lemma ldrop_fwd_rfw: ∀I,L,K,V,i. ⇩[O, i] L ≡ K.ⓑ{I}V → ♯{K, V} < ♯{L, #i}.
+lemma ldrop_fwd_rfw: ∀I,L,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → ♯{K, V} < ♯{L, #i}.
 #I #L #K #V #i #HLK lapply (ldrop_fwd_lw … HLK) -HLK
 normalize in ⊢ (%→?%%); /2 width=1 by le_S_S/
 qed-.
 
 (* Advanced inversion lemmas ************************************************)
 
-fact ldrop_inv_O2_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → e = 0 → L1 = L2.
-#d #e #L1 #L2 #H elim H -d -e -L1 -L2
+fact ldrop_inv_O2_aux: ∀L1,L2,s,d,e. ⇩[s, d, e] L1 ≡ L2 → e = 0 → L1 = L2.
+#L1 #L2 #s #d #e #H elim H -L1 -L2 -d -e
 [ //
 | //
-| #L1 #L2 #I #V #e #_ #_ >commutative_plus normalize #H destruct
-| #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12 #H
+| #I #L1 #L2 #V #e #_ #_ >commutative_plus normalize #H destruct
+| #I #L1 #L2 #V1 #V2 #d #e #_ #HV21 #IHL12 #H
   >(IHL12 H) -L1 >(lift_inv_O2_aux … HV21 … H) -V2 -d -e //
 ]
 qed-.
 
 (* Basic_1: was: drop_gen_refl *)
-lemma ldrop_inv_O2: ∀L1,L2,d. ⇩[d, 0] L1 ≡ L2 → L1 = L2.
-/2 width=4 by ldrop_inv_O2_aux/ qed-.
+lemma ldrop_inv_O2: ∀L1,L2,s,d. ⇩[s, d, 0] L1 ≡ L2 → L1 = L2.
+/2 width=5 by ldrop_inv_O2_aux/ qed-.
 
-lemma ldrop_inv_length_eq: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → |L1| = |L2| → e = 0.
+lemma ldrop_inv_length_eq: ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ L2 → |L1| = |L2| → e = 0.
 #L1 #L2 #d #e #H #HL12 lapply (ldrop_fwd_length_minus4 … H) //
 qed-.
 
-lemma ldrop_inv_refl: ∀L,d,e. ⇩[d, e] L ≡ L → e = 0.
+lemma ldrop_inv_refl: ∀L,d,e. ⇩[Ⓕ, d, e] L ≡ L → e = 0.
 /2 width=5 by ldrop_inv_length_eq/ qed-.
 
+fact ldrop_inv_FT_aux: ∀L1,L2,s,d,e. ⇩[s, d, e] L1 ≡ L2 →
+                       ∀I,K,V. L2 = K.ⓑ{I}V → s = Ⓣ → d = 0 →
+                       ⇩[Ⓕ, d, e] L1 ≡ K.ⓑ{I}V.
+#L1 #L2 #s #d #e #H elim H -L1 -L2 -d -e
+[ #d #e #_ #J #K #W #H destruct
+| #I #L #V #J #K #W #H destruct //
+| #I #L1 #L2 #V #e #_ #IHL12 #J #K #W #H1 #H2 destruct
+  /3 width=1 by ldrop_drop/
+| #I #L1 #L2 #V1 #V2 #d #e #_ #_ #_ #J #K #W #_ #_
+  <plus_n_Sm #H destruct
+]
+qed-.
+
+lemma ldrop_inv_FT: ∀I,L,K,V,e. ⇩[Ⓣ, 0, e] L ≡ K.ⓑ{I}V → ⇩[e] L ≡ K.ⓑ{I}V.
+/2 width=5 by ldrop_inv_FT_aux/ qed.
+
+lemma ldrop_inv_gen: ∀I,L,K,V,s,e. ⇩[s, 0, e] L ≡ K.ⓑ{I}V → ⇩[e] L ≡ K.ⓑ{I}V.
+#I #L #K #V * /2 width=1 by ldrop_inv_FT/
+qed-.
+
+lemma ldrop_inv_T: ∀I,L,K,V,s,e. ⇩[Ⓣ, 0, e] L ≡ K.ⓑ{I}V → ⇩[s, 0, e] L ≡ K.ⓑ{I}V.
+#I #L #K #V * /2 width=1 by ldrop_inv_FT/
+qed-.
+
 (* Basic_1: removed theorems 50:
             drop_ctail drop_skip_flat
             cimp_flat_sx cimp_flat_dx cimp_bind cimp_getl_conf
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_append.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_append.ma
index 2da9f9ed9..1fa09a012 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_append.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_append.ma
@@ -19,23 +19,24 @@ include "basic_2/relocation/ldrop.ma".
 
 (* Properties on append for local environments ******************************)
 
-fact ldrop_O1_append_sn_le_aux: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 →
+fact ldrop_O1_append_sn_le_aux: ∀L1,L2,s,d,e. ⇩[s, d, e] L1 ≡ L2 →
                                 d = 0 → e ≤ |L1| →
-                                ∀L. ⇩[0, e] L @@ L1 ≡ L @@ L2.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize
-/4 width=1 by ldrop_skip_lt, ldrop_ldrop, arith_b1, lt_minus_to_plus_r, monotonic_pred/
+                                ∀L. ⇩[s, 0, e] L @@ L1 ≡ L @@ L2.
+#L1 #L2 #s #d #e #H elim H -L1 -L2 -d -e normalize
+[2,3,4: /4 width=1 by ldrop_skip_lt, ldrop_drop, arith_b1, lt_minus_to_plus_r, monotonic_pred/ ]
+#d #e #_ #_ #H <(le_n_O_to_eq … H) -H //
 qed-.
 
-lemma ldrop_O1_append_sn_le: ∀L1,L2,e. ⇩[0, e] L1 ≡ L2 → e ≤ |L1| →
-                             ∀L. ⇩[0, e] L @@ L1 ≡ L @@ L2.
+lemma ldrop_O1_append_sn_le: ∀L1,L2,s,e. ⇩[s, 0, e] L1 ≡ L2 → e ≤ |L1| →
+                             ∀L. ⇩[s, 0, e] L @@ L1 ≡ L @@ L2.
 /2 width=3 by ldrop_O1_append_sn_le_aux/ qed.
 
 (* Inversion lemmas on append for local environments ************************)
 
-lemma ldrop_O1_inv_append1_ge: ∀K,L1,L2,e. ⇩[0, e] L1 @@ L2 ≡ K →
-                               |L2| ≤ e → ⇩[0, e - |L2|] L1 ≡ K.
+lemma ldrop_O1_inv_append1_ge: ∀K,L1,L2,s,e. ⇩[s, 0, e] L1 @@ L2 ≡ K →
+                               |L2| ≤ e → ⇩[s, 0, e - |L2|] L1 ≡ K.
 #K #L1 #L2 elim L2 -L2 normalize //
-#L2 #I #V #IHL2 #e #H #H1e
+#L2 #I #V #IHL2 #s #e #H #H1e
 elim (ldrop_inv_O1_pair1 … H) -H * #H2e #HL12 destruct
 [ lapply (le_n_O_to_eq … H1e) -H1e -IHL2
   >commutative_plus normalize #H destruct
@@ -43,18 +44,17 @@ elim (ldrop_inv_O1_pair1 … H) -H * #H2e #HL12 destruct
 ]
 qed-.
 
-lemma ldrop_O1_inv_append1_le: ∀K,L1,L2,e. ⇩[0, e] L1 @@ L2 ≡ K → e ≤ |L2| →
-                               ∀K2. ⇩[0, e] L2 ≡ K2 → K = L1 @@ K2.
+lemma ldrop_O1_inv_append1_le: ∀K,L1,L2,s,e. ⇩[s, 0, e] L1 @@ L2 ≡ K → e ≤ |L2| →
+                               ∀K2. ⇩[s, 0, e] L2 ≡ K2 → K = L1 @@ K2.
 #K #L1 #L2 elim L2 -L2 normalize
-[ #e #H1 #H2 #K2 #H3
-  lapply (le_n_O_to_eq … H2) -H2 #H2
-  elim (ldrop_inv_atom1 … H3) -H3 #H3 #_ destruct
+[ #s #e #H1 #H2 #K2 #H3 lapply (le_n_O_to_eq … H2) -H2
+  #H2 elim (ldrop_inv_atom1 … H3) -H3 #H3 #_ destruct
   >(ldrop_inv_O2 … H1) -H1 //
-| #L2 #I #V #IHL2 #e @(nat_ind_plus … e) -e [ -IHL2 ]
+| #L2 #I #V #IHL2 #s #e @(nat_ind_plus … e) -e [ -IHL2 ]
   [ #H1 #_ #K2 #H2
     lapply (ldrop_inv_O2 … H1) -H1 #H1
     lapply (ldrop_inv_O2 … H2) -H2 #H2 destruct //
-  | /4 width=6 by ldrop_inv_ldrop1, le_plus_to_le_r/
+  | /4 width=7 by ldrop_inv_drop1, le_plus_to_le_r/
   ]
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_ldrop.ma
index ce3326a9d..77e7e5b59 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_ldrop.ma
@@ -20,14 +20,14 @@ include "basic_2/relocation/ldrop.ma".
 (* Main properties **********************************************************)
 
 (* Basic_1: was: drop_mono *)
-theorem ldrop_mono: ∀d,e,L,L1. ⇩[d, e] L ≡ L1 →
-                    ∀L2. ⇩[d, e] L ≡ L2 → L1 = L2.
-#d #e #L #L1 #H elim H -d -e -L -L1
-[ #d #L2 #H elim (ldrop_inv_atom1 … H) -H //
-| #K #I #V #L2 #HL12 <(ldrop_inv_O2 … HL12) -L2 //
-| #L #K #I #V #e #_ #IHLK #L2 #H
-  lapply (ldrop_inv_ldrop1 … H) -H /2 width=1 by/
-| #L #K1 #I #T #V1 #d #e #_ #HVT1 #IHLK1 #X #H
+theorem ldrop_mono: ∀L,L1,s1,d,e. ⇩[s1, d, e] L ≡ L1 →
+                    ∀L2,s2. ⇩[s2, d, e] L ≡ L2 → L1 = L2.
+#L #L1 #s1 #d #e #H elim H -L -L1 -d -e
+[ #d #e #He #L2 #s2 #H elim (ldrop_inv_atom1 … H) -H //
+| #I #K #V #L2 #s2 #HL12 <(ldrop_inv_O2 … HL12) -L2 //
+| #I #L #K #V #e #_ #IHLK #L2 #s2 #H
+  lapply (ldrop_inv_drop1 … H) -H /2 width=2 by/
+| #I #L #K1 #T #V1 #d #e #_ #HVT1 #IHLK1 #X #s2 #H
   elim (ldrop_inv_skip1 … H) -H // <minus_plus_m_m #K2 #V2 #HLK2 #HVT2 #H destruct
   >(lift_inj … HVT1 … HVT2) -HVT1 -HVT2
   >(IHLK1 … HLK2) -IHLK1 -HLK2 //
@@ -35,148 +35,154 @@ theorem ldrop_mono: ∀d,e,L,L1. ⇩[d, e] L ≡ L1 →
 qed-.
 
 (* Basic_1: was: drop_conf_ge *)
-theorem ldrop_conf_ge: ∀d1,e1,L,L1. ⇩[d1, e1] L ≡ L1 →
-                       ∀e2,L2. ⇩[0, e2] L ≡ L2 → d1 + e1 ≤ e2 →
-                       ⇩[0, e2 - e1] L1 ≡ L2.
-#d1 #e1 #L #L1 #H elim H -d1 -e1 -L -L1 //
-[ #L #K #I #V #e #_ #IHLK #e2 #L2 #H #He2
-  lapply (ldrop_inv_ldrop1_lt … H ?) -H /2 width=2 by ltn_to_ltO/ #HL2
+theorem ldrop_conf_ge: ∀L,L1,s1,d1,e1. ⇩[s1, d1, e1] L ≡ L1 →
+                       ∀L2,s2,e2. ⇩[s2, 0, e2] L ≡ L2 → d1 + e1 ≤ e2 →
+                       ⇩[s2, 0, e2 - e1] L1 ≡ L2.
+#L #L1 #s1 #d1 #e1 #H elim H -L -L1 -d1 -e1 //
+[ #d #e #_ #L2 #s2 #e2 #H #_ elim (ldrop_inv_atom1 … H) -H
+  #H #He destruct
+  @ldrop_atom #H >He // (**) (* explicit constructor *)
+| #I #L #K #V #e #_ #IHLK #L2 #s2 #e2 #H #He2
+  lapply (ldrop_inv_drop1_lt … H ?) -H /2 width=2 by ltn_to_ltO/ #HL2
   <minus_plus >minus_minus_comm /3 width=1 by monotonic_pred/
-| #L #K #I #V1 #V2 #d #e #_ #_ #IHLK #e2 #L2 #H #Hdee2
+| #I #L #K #V1 #V2 #d #e #_ #_ #IHLK #L2 #s2 #e2 #H #Hdee2
   lapply (transitive_le 1 … Hdee2) // #He2
-  lapply (ldrop_inv_ldrop1_lt … H ?) -H // -He2 #HL2
+  lapply (ldrop_inv_drop1_lt … H ?) -H // -He2 #HL2
   lapply (transitive_le (1 + e) … Hdee2) // #Hee2
-  @ldrop_ldrop_lt >minus_minus_comm /3 width=1 by O, lt_minus_to_plus_r, monotonic_le_minus_r, monotonic_pred/ (**) (* explicit constructor *)
+  @ldrop_drop_lt >minus_minus_comm /3 width=1 by lt_minus_to_plus_r, monotonic_le_minus_r, monotonic_pred/ (**) (* explicit constructor *)
 ]
 qed.
 
 (* Note: apparently this was missing in basic_1 *)
-theorem ldrop_conf_be: ∀L0,L1,d1,e1. ⇩[d1, e1] L0 ≡ L1 →
-                       ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
-                       ∃∃L. ⇩[0, d1 + e1 - e2] L2 ≡ L & ⇩[0, d1] L1 ≡ L.
-#L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
-[ #d1 #L2 #e2 #H #Hd1 #_ elim (ldrop_inv_atom1 … H) -H #H1 #H2 destruct
-  <(le_n_O_to_eq … Hd1) -d1 /2 width=3 by ldrop_atom, ex2_intro/
-| normalize #L #I #V #L2 #e2 #HL2 #_ #He2
+theorem ldrop_conf_be: ∀L0,L1,s1,d1,e1. ⇩[s1, d1, e1] L0 ≡ L1 →
+                       ∀L2,e2. ⇩[e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
+                       ∃∃L. ⇩[s1, 0, d1 + e1 - e2] L2 ≡ L & ⇩[d1] L1 ≡ L.
+#L0 #L1 #s1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
+[ #d1 #e1 #He1 #L2 #e2 #H #Hd1 #_ elim (ldrop_inv_atom1 … H) -H #H #He2 destruct
+  >(He2 ?) in Hd1; // -He2 #Hd1 <(le_n_O_to_eq … Hd1) -d1
+  /4 width=3 by ldrop_atom, ex2_intro/
+| normalize #I #L #V #L2 #e2 #HL2 #_ #He2
   lapply (le_n_O_to_eq … He2) -He2 #H destruct
   lapply (ldrop_inv_O2 … HL2) -HL2 #H destruct /2 width=3 by ldrop_pair, ex2_intro/
-| normalize #L0 #K0 #I #V1 #e1 #HLK0 #IHLK0 #L2 #e2 #H #_ #He21
+| normalize #I #L0 #K0 #V1 #e1 #HLK0 #IHLK0 #L2 #e2 #H #_ #He21
   lapply (ldrop_inv_O1_pair1 … H) -H * * #He2 #HL20
-  [ -IHLK0 -He21 destruct <minus_n_O /3 width=3 by ldrop_ldrop, ex2_intro/
+  [ -IHLK0 -He21 destruct <minus_n_O /3 width=3 by ldrop_drop, ex2_intro/
   | -HLK0 <minus_le_minus_minus_comm //
     elim (IHLK0 … HL20) -L0 /2 width=3 by monotonic_pred, ex2_intro/
   ]
-| #L0 #K0 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHLK0 #L2 #e2 #H #Hd1e2 #He2de1
+| #I #L0 #K0 #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHLK0 #L2 #e2 #H #Hd1e2 #He2de1
   elim (le_inv_plus_l … Hd1e2) #_ #He2
   <minus_le_minus_minus_comm //
-  lapply (ldrop_inv_ldrop1_lt … H ?) -H // #HL02
-  elim (IHLK0 … HL02) -L0 /3 width=3 by ldrop_ldrop, monotonic_pred, ex2_intro/
+  lapply (ldrop_inv_drop1_lt … H ?) -H // #HL02
+  elim (IHLK0 … HL02) -L0 /3 width=3 by ldrop_drop, monotonic_pred, ex2_intro/
 ]
-qed.
+qed-.
 
 (* Note: apparently this was missing in basic_1 *)
-theorem ldrop_conf_le: ∀L0,L1,d1,e1. ⇩[d1, e1] L0 ≡ L1 →
-                       ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
-                       ∃∃L. ⇩[0, e2] L1 ≡ L & ⇩[d1 - e2, e1] L2 ≡ L.
-#L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
-[ #d1 #L2 #e2 #H
-  elim (ldrop_inv_atom1 … H) -H #H destruct /2 width=3 by ldrop_atom, ex2_intro/
-| #K0 #I #V0 #L2 #e2 #H1 #H2
+theorem ldrop_conf_le: ∀L0,L1,s1,d1,e1. ⇩[s1, d1, e1] L0 ≡ L1 →
+                       ∀L2,s2,e2. ⇩[s2, 0, e2] L0 ≡ L2 → e2 ≤ d1 →
+                       ∃∃L. ⇩[s2, 0, e2] L1 ≡ L & ⇩[s1, d1 - e2, e1] L2 ≡ L.
+#L0 #L1 #s1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
+[ #d1 #e1 #He1 #L2 #s2 #e2 #H elim (ldrop_inv_atom1 … H) -H
+  #H #He2 #_ destruct /4 width=3 by ldrop_atom, ex2_intro/
+| #I #K0 #V0 #L2 #s2 #e2 #H1 #H2
   lapply (le_n_O_to_eq … H2) -H2 #H destruct
   lapply (ldrop_inv_pair1 … H1) -H1 #H destruct /2 width=3 by ldrop_pair, ex2_intro/
-| #K0 #K1 #I #V0 #e1 #HK01 #_ #L2 #e2 #H1 #H2
+| #I #K0 #K1 #V0 #e1 #HK01 #_ #L2 #s2 #e2 #H1 #H2
   lapply (le_n_O_to_eq … H2) -H2 #H destruct
-  lapply (ldrop_inv_pair1 … H1) -H1 #H destruct /3 width=3 by ldrop_ldrop, ex2_intro/
-| #K0 #K1 #I #V0 #V1 #d1 #e1 #HK01 #HV10 #IHK01 #L2 #e2 #H #He2d1
+  lapply (ldrop_inv_pair1 … H1) -H1 #H destruct /3 width=3 by ldrop_drop, ex2_intro/
+| #I #K0 #K1 #V0 #V1 #d1 #e1 #HK01 #HV10 #IHK01 #L2 #s2 #e2 #H #He2d1
   elim (ldrop_inv_O1_pair1 … H) -H *
   [ -IHK01 -He2d1 #H1 #H2 destruct /3 width=5 by ldrop_pair, ldrop_skip, ex2_intro/
   | -HK01 -HV10 #He2 #HK0L2
     elim (IHK01 … HK0L2) -IHK01 -HK0L2 /2 width=1 by monotonic_pred/
-    >minus_le_minus_minus_comm /3 width=3 by ldrop_ldrop_lt, ex2_intro/
+    >minus_le_minus_minus_comm /3 width=3 by ldrop_drop_lt, ex2_intro/
   ]
 ]
-qed.
+qed-.
 
+(* Note: with "s2", the conclusion parameter is "s1 ∨ s2" *)
 (* Basic_1: was: drop_trans_ge *)
-theorem ldrop_trans_ge: ∀d1,e1,L1,L. ⇩[d1, e1] L1 ≡ L →
-                        ∀e2,L2. ⇩[0, e2] L ≡ L2 → d1 ≤ e2 → ⇩[0, e1 + e2] L1 ≡ L2.
-#d1 #e1 #L1 #L #H elim H -d1 -e1 -L1 -L //
-[ /3 width=1/
-| #L1 #L2 #I #V1 #V2 #d #e #H_ #_ #IHL12 #e2 #L #H #Hde2
+theorem ldrop_trans_ge: ∀L1,L,s1,d1,e1. ⇩[s1, d1, e1] L1 ≡ L →
+                        ∀L2,e2. ⇩[e2] L ≡ L2 → d1 ≤ e2 → ⇩[s1, 0, e1 + e2] L1 ≡ L2.
+#L1 #L #s1 #d1 #e1 #H elim H -L1 -L -d1 -e1
+[ #d1 #e1 #He1 #L2 #e2 #H #_ elim (ldrop_inv_atom1 … H) -H
+  #H #He2 destruct /4 width=1 by ldrop_atom, eq_f2/
+| /2 width=1 by ldrop_gen/
+| /3 width=1 by ldrop_drop/
+| #I #L1 #L2 #V1 #V2 #d #e #_ #_ #IHL12 #L #e2 #H #Hde2
   lapply (lt_to_le_to_lt 0 … Hde2) // #He2
   lapply (lt_to_le_to_lt … (e + e2) He2 ?) // #Hee2
-  lapply (ldrop_inv_ldrop1_lt … H ?) -H // #HL2
-  @ldrop_ldrop_lt // >le_plus_minus /3 width=1 by monotonic_pred/
+  lapply (ldrop_inv_drop1_lt … H ?) -H // #HL2
+  @ldrop_drop_lt // >le_plus_minus /3 width=1 by monotonic_pred/
 ]
 qed.
 
 (* Basic_1: was: drop_trans_le *)
-theorem ldrop_trans_le: ∀d1,e1,L1,L. ⇩[d1, e1] L1 ≡ L →
-                        ∀e2,L2. ⇩[0, e2] L ≡ L2 → e2 ≤ d1 →
-                        ∃∃L0. ⇩[0, e2] L1 ≡ L0 & ⇩[d1 - e2, e1] L0 ≡ L2.
-#d1 #e1 #L1 #L #H elim H -d1 -e1 -L1 -L
-[ #d #e2 #L2 #H
-  elim (ldrop_inv_atom1 … H) -H /2 width=3 by ldrop_atom, ex2_intro/
-| #K #I #V #e2 #L2 #HL2 #H
-  lapply (le_n_O_to_eq … H) -H #H destruct /2 width=3 by ldrop_pair, ex2_intro/
-| #L1 #L2 #I #V #e #_ #IHL12 #e2 #L #HL2 #H
-  lapply (le_n_O_to_eq … H) -H #H destruct
-  elim (IHL12 … HL2) -IHL12 -HL2 // #L0 #H #HL0
-  lapply (ldrop_inv_O2 … H) -H #H destruct /3 width=5 by ldrop_pair, ldrop_ldrop, ex2_intro/
-| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #IHL12 #e2 #L #H #He2d
+theorem ldrop_trans_le: ∀L1,L,s1,d1,e1. ⇩[s1, d1, e1] L1 ≡ L →
+                        ∀L2,s2,e2. ⇩[s2, 0, e2] L ≡ L2 → e2 ≤ d1 →
+                        ∃∃L0. ⇩[s2, 0, e2] L1 ≡ L0 & ⇩[s1, d1 - e2, e1] L0 ≡ L2.
+#L1 #L #s1 #d1 #e1 #H elim H -L1 -L -d1 -e1
+[ #d1 #e1 #He1 #L2 #s2 #e2 #H #_ elim (ldrop_inv_atom1 … H) -H
+  #H #He2 destruct /4 width=3 by ldrop_atom, ex2_intro/
+| #I #K #V #L2 #s2 #e2 #HL2 #H lapply (le_n_O_to_eq … H) -H
+  #H destruct /2 width=3 by ldrop_pair, ex2_intro/
+| #I #L1 #L2 #V #e #_ #IHL12 #L #s2 #e2 #HL2 #H lapply (le_n_O_to_eq … H) -H
+  #H destruct elim (IHL12 … HL2) -IHL12 -HL2 //
+  #L0 #H #HL0 lapply (ldrop_inv_O2 … H) -H #H destruct
+  /3 width=5 by ldrop_pair, ldrop_drop, ex2_intro/
+| #I #L1 #L2 #V1 #V2 #d #e #HL12 #HV12 #IHL12 #L #s2 #e2 #H #He2d
   elim (ldrop_inv_O1_pair1 … H) -H *
   [ -He2d -IHL12 #H1 #H2 destruct /3 width=5 by ldrop_pair, ldrop_skip, ex2_intro/
   | -HL12 -HV12 #He2 #HL2
-    elim (IHL12 … HL2) -L2 [ >minus_le_minus_minus_comm // /3 width=3 by ldrop_ldrop_lt, ex2_intro/ | /2 width=1 by monotonic_pred/ ]
+    elim (IHL12 … HL2) -L2 [ >minus_le_minus_minus_comm // /3 width=3 by ldrop_drop_lt, ex2_intro/ | /2 width=1 by monotonic_pred/ ]
   ]
 ]
-qed.
-
-(* Basic_1: was: drop_conf_rev *)
-axiom ldrop_div: ∀e1,L1,L. ⇩[0, e1] L1 ≡ L → ∀e2,L2. ⇩[0, e2] L2 ≡ L →
-                 ∃∃L0. ⇩[0, e1] L0 ≡ L2 & ⇩[e1, e2] L0 ≡ L1.
+qed-.
 
 (* Advanced properties ******************************************************)
 
 lemma l_liftable_llstar: ∀R. l_liftable R → ∀l. l_liftable (llstar … R l).
 #R #HR #l #K #T1 #T2 #H @(lstar_ind_r … l T2 H) -l -T2
-[ #L #d #e #_ #U1 #HTU1 #U2 #HTU2 -HR -K
+[ #L #s #d #e #_ #U1 #HTU1 #U2 #HTU2 -HR -K
   >(lift_mono … HTU2 … HTU1) -T1 -U2 -d -e //
-| #l #T #T2 #_ #HT2 #IHT1 #L #d #e #HLK #U1 #HTU1 #U2 #HTU2
-  elim (lift_total T d e) /3 width=11 by lstar_dx/
+| #l #T #T2 #_ #HT2 #IHT1 #L #s #d #e #HLK #U1 #HTU1 #U2 #HTU2
+  elim (lift_total T d e) /3 width=12 by lstar_dx/
 ]
-qed.
+qed-.
 
 (* Basic_1: was: drop_conf_lt *)
-lemma ldrop_conf_lt: ∀d1,e1,L,L1. ⇩[d1, e1] L ≡ L1 →
-                     ∀e2,K2,I,V2. ⇩[0, e2] L ≡ K2. ⓑ{I} V2 →
+lemma ldrop_conf_lt: ∀L,L1,s1,d1,e1. ⇩[s1, d1, e1] L ≡ L1 →
+                     ∀I,K2,V2,s2,e2. ⇩[s2, 0, e2] L ≡ K2.ⓑ{I}V2 →
                      e2 < d1 → let d ≝ d1 - e2 - 1 in
-                     ∃∃K1,V1. ⇩[0, e2] L1 ≡ K1. ⓑ{I} V1 &
-                              ⇩[d, e1] K2 ≡ K1 & ⇧[d, e1] V1 ≡ V2.
-#d1 #e1 #L #L1 #H1 #e2 #K2 #I #V2 #H2 #He2d1
+                     ∃∃K1,V1. ⇩[s2, 0, e2] L1 ≡ K1.ⓑ{I}V1 &
+                              ⇩[s1, d, e1] K2 ≡ K1 & ⇧[d, e1] V1 ≡ V2.
+#L #L1 #s1 #d1 #e1 #H1 #I #K2 #V2 #s2 #e2 #H2 #He2d1
 elim (ldrop_conf_le … H1 … H2) -L /2 width=2 by lt_to_le/ #K #HL1K #HK2
-elim (ldrop_inv_skip1 … HK2) -HK2 /2 width=1 by lt_plus_to_minus_r/ #K1 #V1 #HK21 #HV12 #H destruct /2 width=5 by ex3_2_intro/
-qed.
+elim (ldrop_inv_skip1 … HK2) -HK2 /2 width=1 by lt_plus_to_minus_r/
+#K1 #V1 #HK21 #HV12 #H destruct /2 width=5 by ex3_2_intro/
+qed-.
 
 (* Note: apparently this was missing in basic_1 *)
-lemma ldrop_trans_lt: ∀d1,e1,L1,L. ⇩[d1, e1] L1 ≡ L →
-                      ∀e2,L2,I,V2. ⇩[0, e2] L ≡ L2.ⓑ{I}V2 →
+lemma ldrop_trans_lt: ∀L1,L,s1,d1,e1. ⇩[s1, d1, e1] L1 ≡ L →
+                      ∀I,L2,V2,s2,e2. ⇩[s2, 0, e2] L ≡ L2.ⓑ{I}V2 →
                       e2 < d1 → let d ≝ d1 - e2 - 1 in
-                      ∃∃L0,V0. ⇩[0, e2] L1 ≡ L0.ⓑ{I}V0 &
-                               ⇩[d, e1] L0 ≡ L2 & ⇧[d, e1] V2 ≡ V0.
-#d1 #e1 #L1 #L #HL1 #e2 #L2 #I #V2 #HL2 #Hd21
+                      ∃∃L0,V0. ⇩[s2, 0, e2] L1 ≡ L0.ⓑ{I}V0 &
+                               ⇩[s1, d, e1] L0 ≡ L2 & ⇧[d, e1] V2 ≡ V0.
+#L1 #L #s1 #d1 #e1 #HL1 #I #L2 #V2 #s2 #e2 #HL2 #Hd21
 elim (ldrop_trans_le … HL1 … HL2) -L /2 width=1 by lt_to_le/ #L0 #HL10 #HL02
 elim (ldrop_inv_skip2 … HL02) -HL02 /2 width=1 by lt_plus_to_minus_r/ #L #V1 #HL2 #HV21 #H destruct /2 width=5 by ex3_2_intro/
 qed-.
 
-lemma ldrop_trans_ge_comm: ∀d1,e1,e2,L1,L2,L.
-                           ⇩[d1, e1] L1 ≡ L → ⇩[0, e2] L ≡ L2 → d1 ≤ e2 →
-                           ⇩[0, e2 + e1] L1 ≡ L2.
-#e1 #e1 #e2 >commutative_plus /2 width=5 by ldrop_trans_ge/
+lemma ldrop_trans_ge_comm: ∀L1,L,L2,s1,d1,e1,e2.
+                           ⇩[s1, d1, e1] L1 ≡ L → ⇩[e2] L ≡ L2 → d1 ≤ e2 →
+                           ⇩[s1, 0, e2 + e1] L1 ≡ L2.
+#L1 #L #L2 #s1 #d1 #e1 #e2
+>commutative_plus /2 width=5 by ldrop_trans_ge/
 qed.
 
-lemma ldrop_conf_div: ∀I1,L,K,V1,e1. ⇩[0, e1] L ≡ K. ⓑ{I1} V1 →
-                      ∀I2,V2,e2. ⇩[0, e2] L ≡ K. ⓑ{I2} V2 →
+lemma ldrop_conf_div: ∀I1,L,K,V1,e1. ⇩[e1] L ≡ K.ⓑ{I1}V1 →
+                      ∀I2,V2,e2. ⇩[e2] L ≡ K.ⓑ{I2}V2 →
                       ∧∧ e1 = e2 & I1 = I2 & V1 = V2.
 #I1 #L #K #V1 #e1 #HLK1 #I2 #V2 #e2 #HLK2
 elim (le_or_ge e1 e2) #He
@@ -193,8 +199,8 @@ qed-.
 
 (* Advanced forward lemmas **************************************************)
 
-lemma ldrop_fwd_be: ∀L,K,d,e,i. ⇩[d, e] L ≡ K → |K| ≤ i → i < d → |L| ≤ i.
-#L #K #d #e #i #HLK #HK #Hd elim (lt_or_ge i (|L|)) //
+lemma ldrop_fwd_be: ∀L,K,s,d,e,i. ⇩[s, d, e] L ≡ K → |K| ≤ i → i < d → |L| ≤ i.
+#L #K #s #d #e #i #HLK #HK #Hd elim (lt_or_ge i (|L|)) //
 #HL elim (ldrop_O1_lt … HL) #I #K0 #V #HLK0 -HL
 elim (ldrop_conf_lt … HLK … HLK0) // -HLK -HLK0 -Hd
 #K1 #V1 #HK1 #_ #_ lapply (ldrop_fwd_length_lt2 … HK1) -I -K1 -V1
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma
index 5dafe7a58..0bf892c33 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma
@@ -20,47 +20,53 @@ include "basic_2/relocation/ldrop.ma".
 (* Properties on sn pointwise extension *************************************)
 
 lemma lpx_sn_deliftable_dropable: ∀R. l_deliftable_sn R → dropable_sn (lpx_sn R).
-#R #HR #L1 #K1 #d #e #H elim H -L1 -K1 -d -e
-[ #d #X #H >(lpx_sn_inv_atom1 … H) -H /2 width=3/
-| #K1 #I #V1 #X #H
-  elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct /3 width=5/
-| #L1 #K1 #I #V1 #e #_ #IHLK1 #X #H
-  elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
-  elim (IHLK1 … HL12) -L1 /3 width=3/
-| #L1 #K1 #I #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H
+#R #HR #L1 #K1 #s #d #e #H elim H -L1 -K1 -d -e
+[ #d #e #He #X #H >(lpx_sn_inv_atom1 … H) -H
+  /4 width=3 by ldrop_atom, lpx_sn_atom, ex2_intro/
+| #I #K1 #V1 #X #H elim (lpx_sn_inv_pair1 … H) -H
+  #L2 #V2 #HL12 #HV12 #H destruct
+  /3 width=5 by ldrop_pair, lpx_sn_pair, ex2_intro/
+| #I #L1 #K1 #V1 #e #_ #IHLK1 #X #H elim (lpx_sn_inv_pair1 … H) -H
+  #L2 #V2 #HL12 #HV12 #H destruct
+  elim (IHLK1 … HL12) -L1 /3 width=3 by ldrop_drop, ex2_intro/
+| #I #L1 #K1 #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H
   elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
   elim (HR … HV12 … HLK1 … HWV1) -V1
-  elim (IHLK1 … HL12) -L1 /3 width=5/
+  elim (IHLK1 … HL12) -L1 /3 width=5 by ldrop_skip, lpx_sn_pair, ex2_intro/
 ]
 qed-.
 
 lemma lpx_sn_liftable_dedropable: ∀R. (∀L. reflexive ? (R L)) →
                                   l_liftable R → dedropable_sn (lpx_sn R).
-#R #H1R #H2R #L1 #K1 #d #e #H elim H -L1 -K1 -d -e
-[ #d #X #H >(lpx_sn_inv_atom1 … H) -H /2 width=3/
-| #K1 #I #V1 #X #H
-  elim (lpx_sn_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=5/
-| #L1 #K1 #I #V1 #e #_ #IHLK1 #K2 #HK12
-  elim (IHLK1 … HK12) -K1 /3 width=5/
-| #L1 #K1 #I #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H
+#R #H1R #H2R #L1 #K1 #s #d #e #H elim H -L1 -K1 -d -e
+[ #d #e #He #X #H >(lpx_sn_inv_atom1 … H) -H
+  /4 width=3 by ldrop_atom, lpx_sn_atom, ex2_intro/
+| #I #K1 #V1 #X #H elim (lpx_sn_inv_pair1 … H) -H
+  #K2 #V2 #HK12 #HV12 #H destruct
+  /3 width=5 by ldrop_pair, lpx_sn_pair, ex2_intro/
+| #I #L1 #K1 #V1 #e #_ #IHLK1 #K2 #HK12 elim (IHLK1 … HK12) -K1
+  /3 width=5 by ldrop_drop, lpx_sn_pair, ex2_intro/
+| #I #L1 #K1 #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H
   elim (lpx_sn_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct
   elim (lift_total W2 d e) #V2 #HWV2
   lapply (H2R … HW12 … HLK1 … HWV1 … HWV2) -W1
-  elim (IHLK1 … HK12) -K1 /3 width=5/
+  elim (IHLK1 … HK12) -K1 /3 width=5 by ldrop_skip, lpx_sn_pair, ex2_intro/
 ]
 qed-.
 
-fact lpx_sn_dropable_aux: ∀R,L2,K2,d,e. ⇩[d, e] L2 ≡ K2 → ∀L1. lpx_sn R L1 L2 →
-                          d = 0 → ∃∃K1. ⇩[0, e] L1 ≡ K1 & lpx_sn R K1 K2.
-#R #L2 #K2 #d #e #H elim H -L2 -K2 -d -e
-[ #d #X #H >(lpx_sn_inv_atom2 … H) -H /2 width=3/
-| #K2 #I #V2 #X #H
-  elim (lpx_sn_inv_pair2 … H) -H #K1 #V1 #HK12 #HV12 #H destruct /3 width=5/
-| #L2 #K2 #I #V2 #e #_ #IHLK2 #X #H #_
-  elim (lpx_sn_inv_pair2 … H) -H #L1 #V1 #HL12 #HV12 #H destruct
-  elim (IHLK2 … HL12) -L2 // /3 width=3/
-| #L2 #K2 #I #V2 #W2 #d #e #_ #_ #_ #L1 #_
-  >commutative_plus normalize #H destruct
+fact lpx_sn_dropable_aux: ∀R,L2,K2,s,d,e. ⇩[s, d, e] L2 ≡ K2 → ∀L1. lpx_sn R L1 L2 →
+                          d = 0 → ∃∃K1. ⇩[s, 0, e] L1 ≡ K1 & lpx_sn R K1 K2.
+#R #L2 #K2 #s #d #e #H elim H -L2 -K2 -d -e
+[ #d #e #He #X #H >(lpx_sn_inv_atom2 … H) -H 
+  /4 width=3 by ldrop_atom, lpx_sn_atom, ex2_intro/
+| #I #K2 #V2 #X #H elim (lpx_sn_inv_pair2 … H) -H
+  #K1 #V1 #HK12 #HV12 #H destruct
+  /3 width=5 by ldrop_pair, lpx_sn_pair, ex2_intro/
+| #I #L2 #K2 #V2 #e #_ #IHLK2 #X #H #_ elim (lpx_sn_inv_pair2 … H) -H
+  #L1 #V1 #HL12 #HV12 #H destruct
+  elim (IHLK2 … HL12) -L2 /3 width=3 by ldrop_drop, ex2_intro/
+| #I #L2 #K2 #V2 #W2 #d #e #_ #_ #_ #L1 #_
+  <plus_n_Sm #H destruct
 ]
 qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lsubr.ma
index faf254e36..e96683a80 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lsubr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lsubr.ma
@@ -30,7 +30,7 @@ interpretation
 (* Basic properties *********************************************************)
 
 lemma lsubr_refl: ∀L. L ⊑ L.
-#L elim L -L // /2 width=1/
+#L elim L -L /2 width=1 by lsubr_sort, lsubr_bind/
 qed.
 
 (* Basic inversion lemmas ***************************************************)
@@ -48,8 +48,8 @@ lemma lsubr_inv_atom1: ∀L2. ⋆ ⊑ L2 → L2 = ⋆.
 fact lsubr_inv_abst1_aux: ∀L1,L2. L1 ⊑ L2 → ∀K1,W. L1 = K1.ⓛW →
                           L2 = ⋆ ∨ ∃∃K2. K1 ⊑ K2 & L2 = K2.ⓛW.
 #L1 #L2 * -L1 -L2
-[ #L #K1 #W #H destruct /2 width=1/
-| #I #L1 #L2 #V #HL12 #K1 #W #H destruct /3 width=3/
+[ #L #K1 #W #H destruct /2 width=1 by or_introl/
+| #I #L1 #L2 #V #HL12 #K1 #W #H destruct /3 width=3 by ex2_intro, or_intror/
 | #L1 #L2 #V1 #V2 #_ #K1 #W #H destruct
 ]
 qed-.
@@ -62,7 +62,7 @@ fact lsubr_inv_abbr2_aux: ∀L1,L2. L1 ⊑ L2 → ∀K2,W. L2 = K2.ⓓW →
                           ∃∃K1. K1 ⊑ K2 & L1 = K1.ⓓW.
 #L1 #L2 * -L1 -L2
 [ #L #K2 #W #H destruct
-| #I #L1 #L2 #V #HL12 #K2 #W #H destruct /2 width=3/
+| #I #L1 #L2 #V #HL12 #K2 #W #H destruct /2 width=3 by ex2_intro/
 | #L1 #L2 #V1 #V2 #_ #K2 #W #H destruct
 ]
 qed-.
@@ -74,32 +74,34 @@ lemma lsubr_inv_abbr2: ∀L1,K2,W. L1 ⊑ K2.ⓓW →
 (* Basic forward lemmas *****************************************************)
 
 lemma lsubr_fwd_length: ∀L1,L2. L1 ⊑ L2 → |L2| ≤ |L1|.
-#L1 #L2 #H elim H -L1 -L2 // /2 width=1/
+#L1 #L2 #H elim H -L1 -L2 /2 width=1 by monotonic_le_plus_l/
 qed-.
 
 lemma lsubr_fwd_ldrop2_bind: ∀L1,L2. L1 ⊑ L2 →
-                             ∀I,K2,W,i. ⇩[0, i] L2 ≡ K2.ⓑ{I}W →
-                             (∃∃K1. K1 ⊑ K2 & ⇩[0, i] L1 ≡ K1.ⓑ{I}W) ∨
-                             ∃∃K1,V. K1 ⊑ K2 & ⇩[0, i] L1 ≡ K1.ⓓⓝW.V & I = Abst.
+                             ∀I,K2,W,s,i. ⇩[s, 0, i] L2 ≡ K2.ⓑ{I}W →
+                             (∃∃K1. K1 ⊑ K2 & ⇩[s, 0, i] L1 ≡ K1.ⓑ{I}W) ∨
+                             ∃∃K1,V. K1 ⊑ K2 & ⇩[s, 0, i] L1 ≡ K1.ⓓⓝW.V & I = Abst.
 #L1 #L2 #H elim H -L1 -L2
-[ #L #I #K2 #W #i #H
+[ #L #I #K2 #W #s #i #H
   elim (ldrop_inv_atom1 … H) -H #H destruct
-| #J #L1 #L2 #V #HL12 #IHL12 #I #K2 #W #i #H
+| #J #L1 #L2 #V #HL12 #IHL12 #I #K2 #W #s #i #H
   elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK2 destruct [ -IHL12 | -HL12 ]
-  [ /3 width=3/
-  | elim (IHL12 … HLK2) -IHL12 -HLK2 * /4 width=3/ /4 width=4/
+  [ /3 width=3 by ldrop_pair, ex2_intro, or_introl/
+  | elim (IHL12 … HLK2) -IHL12 -HLK2 *
+    /4 width=4 by ldrop_drop_lt, ex3_2_intro, ex2_intro, or_introl, or_intror/
   ]
-| #L1 #L2 #V1 #V2 #HL12 #IHL12 #I #K2 #W #i #H
+| #L1 #L2 #V1 #V2 #HL12 #IHL12 #I #K2 #W #s #i #H
   elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK2 destruct [ -IHL12 | -HL12 ]
-  [ /3 width=4/
-  | elim (IHL12 … HLK2) -IHL12 -HLK2 * /4 width=3/ /4 width=4/
+  [ /3 width=4 by ldrop_pair, ex3_2_intro, or_intror/
+  | elim (IHL12 … HLK2) -IHL12 -HLK2 *
+    /4 width=4 by ldrop_drop_lt, ex3_2_intro, ex2_intro, or_introl, or_intror/
   ]
 ]
 qed-.
 
 lemma lsubr_fwd_ldrop2_abbr: ∀L1,L2. L1 ⊑ L2 →
-                             ∀K2,V,i. ⇩[0, i] L2 ≡ K2.ⓓV →
-                             ∃∃K1. K1 ⊑ K2 & ⇩[0, i] L1 ≡ K1.ⓓV.
-#L1 #L2 #HL12 #K2 #V #i #HLK2 elim (lsubr_fwd_ldrop2_bind … HL12 … HLK2) -L2 // *
+                             ∀K2,V,s,i. ⇩[s, 0, i] L2 ≡ K2.ⓓV →
+                             ∃∃K1. K1 ⊑ K2 & ⇩[s, 0, i] L1 ≡ K1.ⓓV.
+#L1 #L2 #HL12 #K2 #V #s #i #HLK2 elim (lsubr_fwd_ldrop2_bind … HL12 … HLK2) -L2 // *
 #K1 #W #_ #_ #H destruct
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lsubr_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lsubr_lsubr.ma
index 89be682e1..b7065bae5 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lsubr_lsubr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lsubr_lsubr.ma
@@ -24,9 +24,9 @@ fact lsubr_inv_bind1_aux: ∀L1,L2. L1 ⊑ L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X →
                            | ∃∃K2,V,W. K1 ⊑ K2 & L2 = K2.ⓛW &
                                        I = Abbr & X = ⓝW.V.
 #L1 #L2 * -L1 -L2
-[ #L #J #K1 #X #H destruct /2 width=1/
-| #I #L1 #L2 #V #HL12 #J #K1 #X #H destruct /3 width=3/
-| #L1 #L2 #V #W #HL12 #J #K1 #X #H destruct /3 width=6/
+[ #L #J #K1 #X #H destruct /2 width=1 by or3_intro0/
+| #I #L1 #L2 #V #HL12 #J #K1 #X #H destruct /3 width=3 by or3_intro1, ex2_intro/
+| #L1 #L2 #V #W #HL12 #J #K1 #X #H destruct /3 width=6 by or3_intro2, ex4_3_intro/
 ]
 qed-.
 
@@ -45,9 +45,9 @@ theorem lsubr_trans: Transitive … lsubr.
   lapply (lsubr_inv_atom1 … H) -H //
 | #I #L1 #L #V #_ #IHL1 #X #H
   elim (lsubr_inv_bind1 … H) -H // *
-  #L2 [2: #V2 #W2 ] #HL2 #H1 [ #H2 #H3 ] destruct /3 width=1/
+  #L2 [2: #V2 #W2 ] #HL2 #H1 [ #H2 #H3 ] destruct /3 width=1 by lsubr_bind, lsubr_abst/
 | #L1 #L #V1 #W #_ #IHL1 #X #H
   elim (lsubr_inv_abst1 … H) -H // *
-  #L2 #HL2 #H destruct /3 width=1/
+  #L2 #HL2 #H destruct /3 width=1 by lsubr_abst/
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma
index 75cc5ce57..123529e05 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma
@@ -203,28 +203,28 @@ lemma lsuby_fwd_length: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 → |L2| ≤ |L1|.
 qed-.
 
 lemma lsuby_fwd_ldrop2_be: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 →
-                           ∀I2,K2,W,i. ⇩[0, i] L2 ≡ K2.ⓑ{I2}W →
+                           ∀I2,K2,W,s,i. ⇩[s, 0, i] L2 ≡ K2.ⓑ{I2}W →
                            d ≤ i → i < d + e →
-                           ∃∃I1,K1. K1 ⊑×[0, ⫰(d+e-i)] K2 & ⇩[0, i] L1 ≡ K1.ⓑ{I1}W.
+                           ∃∃I1,K1. K1 ⊑×[0, ⫰(d+e-i)] K2 & ⇩[s, 0, i] L1 ≡ K1.ⓑ{I1}W.
 #L1 #L2 #d #e #H elim H -L1 -L2 -d -e
-[ #L1 #d #e #J2 #K2 #W #i #H
+[ #L1 #d #e #J2 #K2 #W #s #i #H
   elim (ldrop_inv_atom1 … H) -H #H destruct
-| #I1 #I2 #L1 #L2 #V1 #V2 #_ #_ #J2 #K2 #W #i #_ #_ #H
+| #I1 #I2 #L1 #L2 #V1 #V2 #_ #_ #J2 #K2 #W #s #i #_ #_ #H
   elim (ylt_yle_false … H) //
-| #I1 #I2 #L1 #L2 #V #e #HL12 #IHL12 #J2 #K2 #W #i #H #_ >yplus_O1
+| #I1 #I2 #L1 #L2 #V #e #HL12 #IHL12 #J2 #K2 #W #s #i #H #_ >yplus_O1
   elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK1 [ -IHL12 | -HL12 ]
   [ #_ destruct -I2 >ypred_succ
     /2 width=4 by ldrop_pair, ex2_2_intro/
   | lapply (ylt_inv_O1 i ?) /2 width=1 by ylt_inj/
     #H <H -H #H lapply (ylt_inv_succ … H) -H
     #Hie elim (IHL12 … HLK1) -IHL12 -HLK1 // -Hie
-    >yminus_succ <yminus_inj /3 width=4 by ldrop_ldrop_lt, ex2_2_intro/
+    >yminus_succ <yminus_inj /3 width=4 by ldrop_drop_lt, ex2_2_intro/
   ]
-| #I1 #I2 #L1 #L2 #V1 #V2 #d #e #_ #IHL12 #J2 #K2 #W #i #HLK2 #Hdi
+| #I1 #I2 #L1 #L2 #V1 #V2 #d #e #_ #IHL12 #J2 #K2 #W #s #i #HLK2 #Hdi
   elim (yle_inv_succ1 … Hdi) -Hdi
   #Hdi #Hi <Hi >yplus_succ1 #H lapply (ylt_inv_succ … H) -H
-  #Hide lapply (ldrop_inv_ldrop1_lt … HLK2 ?) -HLK2 /2 width=1 by ylt_O/
+  #Hide lapply (ldrop_inv_drop1_lt … HLK2 ?) -HLK2 /2 width=1 by ylt_O/
   #HLK1 elim (IHL12 … HLK1) -IHL12 -HLK1 <yminus_inj >yminus_SO2
-  /4 width=4 by ylt_O, ldrop_ldrop_lt, ex2_2_intro/
+  /4 width=4 by ylt_O, ldrop_drop_lt, ex2_2_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 ceacb2e53..da58e39aa 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
@@ -222,7 +222,7 @@ table {
           }
         ]
         [ { "generic local env. slicing" * } {
-             [ "ldrops ( ⇩*[?] ? ≡ ? )" "ldrops_ldrop" + "ldrops_ldrops" * ]
+             [ "ldrops ( ⇩*[?,?] ? ≡ ? )" "ldrops_ldrop" + "ldrops_ldrops" * ]
           }
         ]
         [ { "generic term relocation" * } {
@@ -260,7 +260,7 @@ table {
           }
         ]
         [ { "basic local env. slicing" * } {
-             [ "ldrop ( ⇩[?,?] ? ≡ ? )" "ldrop_append" + "ldrop_lpx_sn" + "ldrop_ldrop" * ]
+             [ "ldrop ( ⇩[?,?,?] ? ≡ ? )" "ldrop_append" + "ldrop_lpx_sn" + "ldrop_ldrop" * ]
           }
         ]
         [ { "basic term relocation" * } {
diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/bool.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/bool.ma
new file mode 100644
index 000000000..fed25ceda
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/bool.ma
@@ -0,0 +1,30 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "basics/bool.ma".
+include "ground_2/notation/constructors/no_0.ma".
+include "ground_2/notation/constructors/yes_0.ma".
+
+(* BOOLEAN PROPERTIES *******************************************************)
+
+interpretation "boolean false" 'no = false.
+
+interpretation "boolean true" 'yes = true.
+
+lemma orb_false_r: ∀b1,b2:bool. (b1 ∨ b2) = false → b1 = false ∧ b2 = false.
+* normalize /2 width=1 by conj/ #b2 #H destruct
+qed-.
+
+lemma commutative_orb: commutative … orb.
+* * // qed.
diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/no_0.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/no_0.ma
new file mode 100644
index 000000000..af692211e
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/no_0.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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "Ⓕ"
+  non associative with precedence 55
+  for @{'no}.
diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/yes_0.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/yes_0.ma
new file mode 100644
index 000000000..c321749ae
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/yes_0.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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "Ⓣ"
+  non associative with precedence 55
+  for @{'yes}.