From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 27 Oct 2014 19:39:37 +0000 (+0000)
Subject: - the trace is explicit in all auto tactics with depth > 1
X-Git-Tag: make_still_working~809
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=37e1b4f314ffae815beca71300688040f8da6939;p=helm.git

- the trace is explicit in all auto tactics with depth > 1
- one bug fixed
- the renaming continues ...
---

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
index 889659759..6881d9c92 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
@@ -52,12 +52,12 @@ lemma cprs_refl: ∀G,L,T. ⦃G, L⦄ ⊢ T ➡* T.
 
 lemma cprs_strap1: ∀G,L,T1,T,T2.
                    ⦃G, L⦄ ⊢ T1 ➡* T → ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T1 ➡* T2.
-normalize /2 width=3 by step/ qed.
+normalize /2 width=3 by step/ qed-.
 
 (* Basic_1: was: pr3_step *)
 lemma cprs_strap2: ∀G,L,T1,T,T2.
                    ⦃G, L⦄ ⊢ T1 ➡ T → ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 ➡* T2.
-normalize /2 width=3 by TC_strap/ qed.
+normalize /2 width=3 by TC_strap/ qed-.
 
 lemma lsubr_cprs_trans: ∀G. lsub_trans … (cprs G) lsubr.
 /3 width=5 by lsubr_cpr_trans, LTC_lsub_trans/
@@ -122,7 +122,7 @@ qed-.
 (* Basic_1: was: pr3_gen_cast *)
 lemma cprs_inv_cast1: ∀G,L,W1,T1,U2. ⦃G, L⦄ ⊢ ⓝW1.T1 ➡* U2 → ⦃G, L⦄ ⊢ T1 ➡* U2 ∨
                       ∃∃W2,T2. ⦃G, L⦄ ⊢ W1 ➡* W2 & ⦃G, L⦄ ⊢ T1 ➡* T2 & U2 = ⓝW2.T2.
-#G #L #W1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/
+#G #L #W1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5 by ex3_2_intro, or_intror/
 #U2 #U #_ #HU2 * /3 width=3 by cprs_strap1, or_introl/ *
 #W #T #HW1 #HT1 #H destruct
 elim (cpr_inv_cast1 … HU2) -HU2 /3 width=3 by cprs_strap1, or_introl/ *
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_vector.ma
index 733666659..5b4d465cb 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_vector.ma
@@ -34,9 +34,9 @@ normalize // qed-.
 
 lemma csx_fwd_applv: ∀h,g,G,L,T,Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Ⓐ Vs.T →
                      ⦃G, L⦄ ⊢ ⬊*[h, g] Vs ∧ ⦃G, L⦄ ⊢ ⬊*[h, g] T.
-#h #g #G #L #T #Vs elim Vs -Vs /2 width=1/
+#h #g #G #L #T #Vs elim Vs -Vs /2 width=1 by conj/
 #V #Vs #IHVs #HVs
 lapply (csx_fwd_pair_sn … HVs) #HV
 lapply (csx_fwd_flat_dx … HVs) -HVs #HVs
-elim (IHVs HVs) -IHVs -HVs /3 width=1/
+elim (IHVs HVs) -IHVs -HVs /3 width=1 by conj/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_aaa.ma
index 6ff7ee804..3428478ea 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_aaa.ma
@@ -25,21 +25,21 @@ include "basic_2/computation/lsubc_drops.ma".
 (* Basic_1: was: sc3_arity_csubc *)
 theorem acr_aaa_csubc_lifts: ∀RR,RS,RP.
                              gcp RR RS RP → gcr RR RS RP RP →
-                             ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L0,des. ⬇*[Ⓕ, des] L0 ≡ L1 →
-                             ∀T0. ⬆*[des] T ≡ T0 → ∀L2. G ⊢ L2 ⫃[RP] L0 →
+                             ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L0,cs. ⬇*[Ⓕ, cs] L0 ≡ L1 →
+                             ∀T0. ⬆*[cs] T ≡ T0 → ∀L2. G ⊢ L2 ⫃[RP] L0 →
                              ⦃G, L2, T0⦄ ϵ[RP] 〚A〛.
 #RR #RS #RP #H1RP #H2RP #G #L1 #T #A #H elim H -G -L1 -T -A
-[ #G #L #k #L0 #des #HL0 #X #H #L2 #HL20
+[ #G #L #k #L0 #cs #HL0 #X #H #L2 #HL20
   >(lifts_inv_sort1 … H) -H
   lapply (acr_gcr … H1RP H2RP (⓪)) #HAtom
   lapply (s4 … HAtom G L2 (◊)) /2 width=1 by/
-| #I #G #L1 #K1 #V1 #B #i #HLK1 #HKV1B #IHB #L0 #des #HL01 #X #H #L2 #HL20
+| #I #G #L1 #K1 #V1 #B #i #HLK1 #HKV1B #IHB #L0 #cs #HL01 #X #H #L2 #HL20
   lapply (acr_gcr … H1RP H2RP B) #HB
   elim (lifts_inv_lref1 … H) -H #i1 #Hi1 #H destruct
   lapply (drop_fwd_drop2 … HLK1) #HK1b
-  elim (drops_drop_trans … HL01 … HLK1) #X #des1 #i0 #HL0 #H #Hi0 #Hcs1
+  elim (drops_drop_trans … HL01 … HLK1) #X #cs1 #i0 #HL0 #H #Hi0 #Hcs1
   >(at_mono … Hi1 … Hi0) -i1
-  elim (drops_inv_skip2 … Hcs1 … H) -des1 #K0 #V0 #des0 #Hcs0 #HK01 #HV10 #H destruct
+  elim (drops_inv_skip2 … Hcs1 … H) -cs1 #K0 #V0 #cs0 #Hcs0 #HK01 #HV10 #H destruct
   elim (lsubc_drop_O1_trans … HL20 … HL0) -HL0 #X #HLK2 #H
   elim (lsubc_inv_pair2 … H) -H *
   [ #K2 #HK20 #H destruct
@@ -56,24 +56,24 @@ theorem acr_aaa_csubc_lifts: ∀RR,RS,RP.
     lapply (s5 … HB ? G ? ? (◊) … (ⓝV3.V) … HLK2) /2 width=1 by lift_flat/
     lapply (s7 … HB G L2 (◊)) /3 width=7 by gcr_lift/
   ]
-| #a #G #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20
+| #a #G #L #V #T #B #A #_ #_ #IHB #IHA #L0 #cs #HL0 #X #H #L2 #HL20
   elim (lifts_inv_bind1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct
   lapply (acr_gcr … H1RP H2RP A) #HA
   lapply (acr_gcr … H1RP H2RP B) #HB
   lapply (s1 … HB) -HB #HB
   lapply (s6 … HA G L2 (◊) (◊)) /4 width=5 by lsubc_pair, drops_skip, liftv_nil/
-| #a #G #L #W #T #B #A #HLWB #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL02
+| #a #G #L #W #T #B #A #HLWB #_ #IHB #IHA #L0 #cs #HL0 #X #H #L2 #HL02
   elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
   @(acr_abst  … H1RP H2RP) /2 width=5 by/
-  #L3 #V3 #W3 #T3 #des3 #HL32 #HW03 #HT03 #H1B #H2B
+  #L3 #V3 #W3 #T3 #cs3 #HL32 #HW03 #HT03 #H1B #H2B
   elim (drops_lsubc_trans … H1RP … HL32 … HL02) -L2 #L2 #HL32 #HL20
-  lapply (aaa_lifts … L2 W3 … (des @@ des3) … HLWB) -HLWB /2 width=4 by drops_trans, lifts_trans/ #HLW2B
-  @(IHA (L2. ⓛW3) … (des + 1 @@ des3 + 1)) -IHA
+  lapply (aaa_lifts … L2 W3 … (cs @@ cs3) … HLWB) -HLWB /2 width=4 by drops_trans, lifts_trans/ #HLW2B
+  @(IHA (L2. ⓛW3) … (cs + 1 @@ cs3 + 1)) -IHA
   /3 width=5 by lsubc_beta, drops_trans, drops_skip, lifts_trans/
-| #G #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20
+| #G #L #V #T #B #A #_ #_ #IHB #IHA #L0 #cs #HL0 #X #H #L2 #HL20
   elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct
   /3 width=10 by drops_nil, lifts_nil/
-| #G #L #V #T #A #_ #_ #IH1A #IH2A #L0 #des #HL0 #X #H #L2 #HL20
+| #G #L #V #T #A #_ #_ #IH1A #IH2A #L0 #cs #HL0 #X #H #L2 #HL20
   elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct
   lapply (acr_gcr … H1RP H2RP A) #HA
   lapply (s7 … HA G L2 (◊)) /3 width=5 by/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_cr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_cr.ma
index 1da427f5b..dc9c4498e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_cr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_cr.ma
@@ -62,8 +62,8 @@ record gcr (RR:relation4 genv lenv term term) (RS:relation term) (RP,C:candidate
 
 (* the functional construction for candidates *)
 definition cfun: candidate → candidate → candidate ≝
-                 λC1,C2,G,K,T. ∀L,W,U,des.
-                 ⬇*[Ⓕ, des] L ≡ K → ⬆*[des] T ≡ U → C1 G L W → C2 G L (ⓐW.U).
+                 λC1,C2,G,K,T. ∀L,W,U,cs.
+                 ⬇*[Ⓕ, cs] L ≡ K → ⬆*[cs] T ≡ U → C1 G L W → C2 G L (ⓐW.U).
 
 (* the reducibility candidate associated to an atomic arity *)
 let rec acr (RP:candidate) (A:aarity) on A: candidate ≝
@@ -102,44 +102,44 @@ lemma acr_gcr: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP →
   [ lapply (s2 … IHB G L (◊) … HK) //
   | /3 width=6 by s1, cp3/
   ]
-| #G #L #Vs #HVs #T #H1T #H2T #L0 #V0 #X #des #HL0 #H #HB
+| #G #L #Vs #HVs #T #H1T #H2T #L0 #V0 #X #cs #HL0 #H #HB
   elim (lifts_inv_applv1 … H) -H #V0s #T0 #HV0s #HT0 #H destruct
   lapply (s1 … IHB … HB) #HV0
   @(s2 … IHA … (V0 @ V0s))
   /3 width=14 by gcp2_lifts_all, gcp2_lifts, gcp0_lifts, lifts_simple_dx, conj/
-| #a #G #L #Vs #U #T #W #HA #L0 #V0 #X #des #HL0 #H #HB
+| #a #G #L #Vs #U #T #W #HA #L0 #V0 #X #cs #HL0 #H #HB
   elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
   elim (lifts_inv_flat1 … HY) -HY #U0 #X #HU0 #HX #H destruct
   elim (lifts_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT0 #H destruct
   @(s3 … IHA … (V0 @ V0s)) /5 width=6 by lifts_applv, lifts_flat, lifts_bind/
-| #G #L #Vs #HVs #k #L0 #V0 #X #des #HL0 #H #HB
+| #G #L #Vs #HVs #k #L0 #V0 #X #cs #HL0 #H #HB
   elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
   >(lifts_inv_sort1 … HY) -Y
   lapply (s1 … IHB … HB) #HV0
   @(s4 … IHA … (V0 @ V0s)) /3 width=7 by gcp2_lifts_all, conj/
-| #I #G #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #L0 #V0 #X #des #HL0 #H #HB
+| #I #G #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #L0 #V0 #X #cs #HL0 #H #HB
   elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
   elim (lifts_inv_lref1 … HY) -HY #i0 #Hi0 #H destruct
-  elim (drops_drop_trans … HL0 … HLK) #X #des0 #i1 #HL02 #H #Hi1 #Hcs0
+  elim (drops_drop_trans … HL0 … HLK) #X #cs0 #i1 #HL02 #H #Hi1 #Hcs0
   >(at_mono … Hi1 … Hi0) in HL02; -i1 #HL02
-  elim (drops_inv_skip2 … Hcs0 … H) -H -des0 #L2 #W1 #des0 #Hcs0 #HLK #HVW1 #H destruct
+  elim (drops_inv_skip2 … Hcs0 … H) -H -cs0 #L2 #W1 #cs0 #Hcs0 #HLK #HVW1 #H destruct
   elim (lift_total W1 0 (i0 + 1)) #W2 #HW12
   elim (lifts_lift_trans  … Hcs0 … HVW1 … HW12) // -Hcs0 -Hi0 #V3 #HV13 #HVW2
   >(lift_mono … HV13 … HV12) in HVW2; -V3 #HVW2
   @(s5 … IHA … (V0 @ V0s) … HW12 HL02) /3 width=5 by lifts_applv/
-| #G #L #V1s #V2s #HV12s #a #V #T #HA #HV #L0 #V10 #X #des #HL0 #H #HB
+| #G #L #V1s #V2s #HV12s #a #V #T #HA #HV #L0 #V10 #X #cs #HL0 #H #HB
   elim (lifts_inv_applv1 … H) -H #V10s #Y #HV10s #HY #H destruct
   elim (lifts_inv_bind1 … HY) -HY #V0 #T0 #HV0 #HT0 #H destruct
   elim (lift_total V10 0 1) #V20 #HV120
   elim (liftv_total 0 1 V10s) #V20s #HV120s
   @(s6 … IHA … (V10 @ V10s) (V20 @ V20s)) /3 width=7 by gcp2_lifts, liftv_cons/
-  @(HA … (des + 1)) /2 width=2 by drops_skip/
+  @(HA … (cs + 1)) /2 width=2 by drops_skip/
   [ @lifts_applv //
     elim (liftsv_liftv_trans_le … HV10s … HV120s) -V10s #V10s #HV10s #HV120s
     >(liftv_mono … HV12s … HV10s) -V1s //
   | @(gcr_lift … H1RP … HB … HV120) /2 width=2 by drop_drop/
   ]
-| #G #L #Vs #T #W #HA #HW #L0 #V0 #X #des #HL0 #H #HB
+| #G #L #Vs #T #W #HA #HW #L0 #V0 #X #cs #HL0 #H #HB
   elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
   elim (lifts_inv_flat1 … HY) -HY #W0 #T0 #HW0 #HT0 #H destruct
   @(s7 … IHA … (V0 @ V0s)) /3 width=5 by lifts_applv/
@@ -148,11 +148,11 @@ qed.
 
 lemma acr_abst: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP →
                 ∀a,G,L,W,T,A,B. ⦃G, L, W⦄ ϵ[RP] 〚B〛 → (
-                   ∀L0,V0,W0,T0,des. ⬇*[Ⓕ, des] L0 ≡ L → ⬆*[des] W ≡ W0 → ⬆*[des + 1] T ≡ T0 →
+                   ∀L0,V0,W0,T0,cs. ⬇*[Ⓕ, cs] L0 ≡ L → ⬆*[cs] W ≡ W0 → ⬆*[cs + 1] T ≡ T0 →
                                    ⦃G, L0, V0⦄ ϵ[RP] 〚B〛 → ⦃G, L0, W0⦄ ϵ[RP] 〚B〛 → ⦃G, L0.ⓓⓝW0.V0, T0⦄ ϵ[RP] 〚A〛
                 ) →
                 ⦃G, L, ⓛ{a}W.T⦄ ϵ[RP] 〚②B.A〛.
-#RR #RS #RP #H1RP #H2RP #a #G #L #W #T #A #B #HW #HA #L0 #V0 #X #des #HL0 #H #HB
+#RR #RS #RP #H1RP #H2RP #a #G #L #W #T #A #B #HW #HA #L0 #V0 #X #cs #HL0 #H #HB
 lapply (acr_gcr … H1RP H2RP A) #HCA
 lapply (acr_gcr … H1RP H2RP B) #HCB
 elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs.ma
index ddf4e24ca..4bc12d246 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs.ma
@@ -43,16 +43,16 @@ qed-.
 (* Basic properties *********************************************************)
 
 lemma lpr_lprs: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L1⦄ ⊢ ➡* L2.
-/2 width=1/ qed.
+/2 width=1 by inj/ qed.
 
 lemma lprs_refl: ∀G,L. ⦃G, L⦄ ⊢ ➡* L.
-/2 width=1/ qed.
+/2 width=1 by lpr_lprs/ qed.
 
 lemma lprs_strap1: ∀G,L1,L,L2. ⦃G, L1⦄ ⊢ ➡* L → ⦃G, L⦄ ⊢ ➡ L2 → ⦃G, L1⦄ ⊢ ➡* L2.
-/2 width=3/ qed.
+/2 width=3 by step/ qed-.
 
 lemma lprs_strap2: ∀G,L1,L,L2. ⦃G, L1⦄ ⊢ ➡ L → ⦃G, L⦄ ⊢ ➡* L2 → ⦃G, L1⦄ ⊢ ➡* L2.
-/2 width=3/ qed.
+/2 width=3 by TC_strap/ qed-.
 
 lemma lprs_pair_refl: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → ∀I,V. ⦃G, L1.ⓑ{I}V⦄ ⊢ ➡* L2.ⓑ{I}V.
 /2 width=1 by TC_lpx_sn_pair_refl/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_lprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_lprs.ma
index 1da198d4e..1bb611012 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_lprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_lprs.ma
@@ -28,4 +28,4 @@ theorem lprs_conf: ∀G. confluent2 … (lprs G) (lprs G).
 /3 width=3 by TC_confluent2, lpr_conf/ qed-.
 
 theorem lprs_trans: ∀G. Transitive … (lprs G).
-/2 width=3/ qed-.
+/2 width=3 by trans_TC/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drops.ma
index f76065b80..df89d984f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drops.ma
@@ -20,11 +20,11 @@ include "basic_2/computation/lsubc_drop.ma".
 
 (* Basic_1: was: csubc_drop1_conf_rev *)
 lemma drops_lsubc_trans: ∀RR,RS,RP. gcp RR RS RP →
-                         ∀G,L1,K1,des. ⬇*[Ⓕ, des] L1 ≡ K1 → ∀K2. G ⊢ K1 ⫃[RP] K2 →
-                         ∃∃L2. G ⊢ L1 ⫃[RP] L2 & ⬇*[Ⓕ, des] L2 ≡ K2.
-#RR #RS #RP #Hgcp #G #L1 #K1 #des #H elim H -L1 -K1 -des
+                         ∀G,L1,K1,cs. ⬇*[Ⓕ, cs] L1 ≡ K1 → ∀K2. G ⊢ K1 ⫃[RP] K2 →
+                         ∃∃L2. G ⊢ L1 ⫃[RP] L2 & ⬇*[Ⓕ, cs] L2 ≡ K2.
+#RR #RS #RP #Hgcp #G #L1 #K1 #cs #H elim H -L1 -K1 -cs
 [ /2 width=3 by drops_nil, ex2_intro/
-| #L1 #L #K1 #des #l #m #_ #HLK1 #IHL #K2 #HK12
+| #L1 #L #K1 #cs #l #m #_ #HLK1 #IHL #K2 #HK12
   elim (drop_lsubc_trans … Hgcp … HLK1 … HK12) -Hgcp -K1 #K #HLK #HK2
   elim (IHL … HLK) -IHL -HLK /3 width=5 by drops_cons, ex2_intro/
 ]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc.ma b/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc.ma
index 116e15950..1268d8887 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc.ma
@@ -27,14 +27,14 @@ interpretation
 (* Basic properties *********************************************************)
 
 lemma cpc_refl: ∀G,L. reflexive … (cpc G L).
-/2 width=1/ qed.
+/2 width=1 by or_intror/ qed.
 
 lemma cpc_sym: ∀G,L. symmetric … (cpc L G).
-#G #L #T1 #T2 * /2 width=1/
-qed.
+#G #L #T1 #T2 * /2 width=1 by or_introl, or_intror/
+qed-.
 
 (* Basic forward lemmas *****************************************************)
 
 lemma cpc_fwd_cpr: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌ T2 → ∃∃T. ⦃G, L⦄ ⊢ T1 ➡ T & ⦃G, L⦄ ⊢ T2 ➡ T.
-#G #L #T1 #T2 * /2 width=3/
+#G #L #T1 #T2 * /2 width=3 by ex2_intro/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc_cpc.ma b/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc_cpc.ma
index 714d3e712..14518aaab 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc_cpc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc_cpc.ma
@@ -20,4 +20,4 @@ include "basic_2/conversion/cpc.ma".
 
 theorem cpc_conf: ∀G,L,T0,T1,T2. ⦃G, L⦄ ⊢ T0 ⬌ T1 → ⦃G, L⦄ ⊢ T0 ⬌ T2 →
                   ∃∃T. ⦃G, L⦄ ⊢ T1 ⬌ T & ⦃G, L⦄ ⊢ T2 ⬌ T.
-/3 width=3/ qed-.
+/3 width=3 by cpc_sym, ex2_intro/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma
index c979cedde..cec1db1bc 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma
@@ -45,7 +45,8 @@ lemma cpcs_refl: ∀G,L. reflexive … (cpcs G L).
 
 (* Basic_1: was: pc3_s *)
 lemma cpcs_sym: ∀G,L. symmetric … (cpcs G L).
-#G #L @TC_symmetric // qed-. (**) (* auto fails even after normalize *)
+normalize /3 width=1 by cpc_sym, TC_symmetric/
+qed-.
 
 lemma cpc_cpcs: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌ T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
 /2 width=1 by inj/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma
index cec15c818..0afb82db5 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma
@@ -126,6 +126,6 @@ qed-.
 lemma lenv_ind_alt: ∀R:predicate lenv.
                     R (⋆) → (∀I,L,T. R L → R (ⓑ{I}T.L)) →
                     ∀L. R L.
-#R #IH1 #IH2 #L @(f_ind … length … L) -L #n #IHn * // -IH1
+#R #IH1 #IH2 #L @(f_ind … length … L) -L #x #IHx * // -IH1
 #L #I #V normalize #H destruct elim (lpair_ltail L I V) /3 width=1 by/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_weight.ma
index 642a3d1b8..9bd6e8260 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_weight.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_weight.ma
@@ -27,7 +27,7 @@ interpretation "weight (local environment)" 'Weight L = (lw L).
 (* Basic properties *********************************************************)
 
 lemma lw_pair: ∀I,L,V. ♯{L} < ♯{L.ⓑ{I}V}.
-/3 width=1/ qed.
+/3 width=1 by lt_plus_to_minus_r, monotonic_lt_plus_r/ qed.
 
 (* Basic_1: removed theorems 4: clt_cong clt_head clt_thead clt_wf_ind *)
 (* Basic_1: removed local theorems 1: clt_wf__q_ind *)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/term_simple.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/term_simple.ma
index fba6617b4..6bffbf4fa 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/term_simple.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/term_simple.ma
@@ -34,9 +34,9 @@ fact simple_inv_bind_aux: ∀T. 𝐒⦃T⦄ → ∀a,J,W,U. T = ⓑ{a,J} W. U 
 qed.
 
 lemma simple_inv_bind: ∀a,I,V,T. 𝐒⦃ⓑ{a,I} V. T⦄ → ⊥.
-/2 width=7/ qed-.
+/2 width=7 by simple_inv_bind_aux/ qed-.
 
 lemma simple_inv_pair: ∀I,V,T.  𝐒⦃②{I}V.T⦄ → ∃J. I = Flat2 J.
-* /2 width=2/ #a #I #V #T #H
+* /2 width=2 by ex_intro/ #a #I #V #T #H
 elim (simple_inv_bind … H)
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/drops.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/drops.ma
index c6edbf3ed..53253e55e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/drops.ma
@@ -22,12 +22,12 @@ include "basic_2/multiple/lifts_vector.ma".
 
 inductive drops (s:bool): list2 nat nat → relation lenv ≝
 | drops_nil : ∀L. drops s (◊) L L
-| drops_cons: ∀L1,L,L2,des,l,m.
-              drops s des L1 L → ⬇[s, l, m] L ≡ L2 → drops s ({l, m} @ des) L1 L2
+| drops_cons: ∀L1,L,L2,cs,l,m.
+              drops s cs L1 L → ⬇[s, l, m] L ≡ L2 → drops s ({l, m} @ cs) L1 L2
 .
 
 interpretation "iterated slicing (local environment) abstract"
-   'RDropStar s des T1 T2 = (drops s des T1 T2).
+   'RDropStar s cs T1 T2 = (drops s cs T1 T2).
 (*
 interpretation "iterated slicing (local environment) general"
    'RDropStar des T1 T2 = (drops true des T1 T2).
@@ -38,57 +38,57 @@ definition d_liftable1: relation2 lenv term → predicate bool ≝
                         ∀U. ⬆[l, m] T ≡ U → R L U.
 
 definition d_liftables1: relation2 lenv term → predicate bool ≝
-                         λR,s. ∀L,K,des. ⬇*[s, des] L ≡ K →
-                         ∀T,U. ⬆*[des] T ≡ U → R K T → R L U.
+                         λR,s. ∀L,K,cs. ⬇*[s, cs] L ≡ K →
+                         ∀T,U. ⬆*[cs] T ≡ U → R K T → R L U.
 
 definition d_liftables1_all: relation2 lenv term → predicate bool ≝
-                             λR,s. ∀L,K,des. ⬇*[s, des] L ≡ K →
-                             ∀Ts,Us. ⬆*[des] Ts ≡ Us → 
+                             λR,s. ∀L,K,cs. ⬇*[s, cs] L ≡ K →
+                             ∀Ts,Us. ⬆*[cs] Ts ≡ Us → 
                              all … (R K) Ts → all … (R L) Us.
 
 (* Basic inversion lemmas ***************************************************)
 
-fact drops_inv_nil_aux: ∀L1,L2,s,des. ⬇*[s, des] L1 ≡ L2 → des = ◊ → L1 = L2.
-#L1 #L2 #s #des * -L1 -L2 -des //
-#L1 #L #L2 #l #m #des #_ #_ #H destruct
+fact drops_inv_nil_aux: ∀L1,L2,s,cs. ⬇*[s, cs] L1 ≡ L2 → cs = ◊ → L1 = L2.
+#L1 #L2 #s #cs * -L1 -L2 -cs //
+#L1 #L #L2 #l #m #cs #_ #_ #H destruct
 qed-.
 
 (* Basic_1: was: drop1_gen_pnil *)
 lemma drops_inv_nil: ∀L1,L2,s. ⬇*[s, ◊] L1 ≡ L2 → L1 = L2.
 /2 width=4 by drops_inv_nil_aux/ qed-.
 
-fact drops_inv_cons_aux: ∀L1,L2,s,des. ⬇*[s, des] L1 ≡ L2 →
-                         ∀l,m,tl. des = {l, m} @ tl →
+fact drops_inv_cons_aux: ∀L1,L2,s,cs. ⬇*[s, cs] L1 ≡ L2 →
+                         ∀l,m,tl. cs = {l, m} @ tl →
                          ∃∃L. ⬇*[s, tl] L1 ≡ L & ⬇[s, l, m] L ≡ L2.
-#L1 #L2 #s #des * -L1 -L2 -des
+#L1 #L2 #s #cs * -L1 -L2 -cs
 [ #L #l #m #tl #H destruct
-| #L1 #L #L2 #des #l #m #HT1 #HT2 #l0 #m0 #tl #H destruct
+| #L1 #L #L2 #cs #l #m #HT1 #HT2 #l0 #m0 #tl #H destruct
   /2 width=3 by ex2_intro/
 ]
 qed-.
 
 (* Basic_1: was: drop1_gen_pcons *)
-lemma drops_inv_cons: ∀L1,L2,s,l,m,des. ⬇*[s, {l, m} @ des] L1 ≡ L2 →
-                      ∃∃L. ⬇*[s, des] L1 ≡ L & ⬇[s, l, m] L ≡ L2.
+lemma drops_inv_cons: ∀L1,L2,s,l,m,cs. ⬇*[s, {l, m} @ cs] L1 ≡ L2 →
+                      ∃∃L. ⬇*[s, cs] L1 ≡ L & ⬇[s, l, m] L ≡ L2.
 /2 width=3 by drops_inv_cons_aux/ qed-.
 
-lemma drops_inv_skip2: ∀I,s,des,des2,i. des ▭ i ≡ des2 →
-                       ∀L1,K2,V2. ⬇*[s, des2] L1 ≡ K2. ⓑ{I} V2 →
-                       ∃∃K1,V1,des1. des + 1 ▭ i + 1 ≡ des1 + 1 &
-                                     ⬇*[s, des1] K1 ≡ K2 &
-                                     ⬆*[des1] V2 ≡ V1 &
+lemma drops_inv_skip2: ∀I,s,cs,cs2,i. cs ▭ i ≡ cs2 →
+                       ∀L1,K2,V2. ⬇*[s, cs2] L1 ≡ K2. ⓑ{I} V2 →
+                       ∃∃K1,V1,cs1. cs + 1 ▭ i + 1 ≡ cs1 + 1 &
+                                     ⬇*[s, cs1] K1 ≡ K2 &
+                                     ⬆*[cs1] V2 ≡ V1 &
                                      L1 = K1. ⓑ{I} V1.
-#I #s #des #des2 #i #H elim H -des -des2 -i
+#I #s #cs #cs2 #i #H elim H -cs -cs2 -i
 [ #i #L1 #K2 #V2 #H
   >(drops_inv_nil … H) -L1 /2 width=7 by lifts_nil, minuss_nil, ex4_3_intro, drops_nil/
-| #des #des2 #l #m #i #Hil #_ #IHcs2 #L1 #K2 #V2 #H
+| #cs #cs2 #l #m #i #Hil #_ #IHcs2 #L1 #K2 #V2 #H
   elim (drops_inv_cons … H) -H #L #HL1 #H
   elim (drop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ #K #V >minus_plus #HK2 #HV2 #H destruct
-  elim (IHcs2 … HL1) -IHcs2 -HL1 #K1 #V1 #des1 #Hcs1 #HK1 #HV1 #X destruct
+  elim (IHcs2 … HL1) -IHcs2 -HL1 #K1 #V1 #cs1 #Hcs1 #HK1 #HV1 #X destruct
   @(ex4_3_intro … K1 V1 … ) // [3,4: /2 width=7 by lifts_cons, drops_cons/ | skip ]
   normalize >plus_minus /3 width=1 by minuss_lt, lt_minus_to_plus/ (**) (* explicit constructors *)
-| #des #des2 #l #m #i #Hil #_ #IHcs2 #L1 #K2 #V2 #H
-  elim (IHcs2 … H) -IHcs2 -H #K1 #V1 #des1 #Hcs1 #HK1 #HV1 #X destruct
+| #cs #cs2 #l #m #i #Hil #_ #IHcs2 #L1 #K2 #V2 #H
+  elim (IHcs2 … H) -IHcs2 -H #K1 #V1 #cs1 #Hcs1 #HK1 #HV1 #X destruct
   /4 width=7 by minuss_ge, ex4_3_intro, le_S_S/
 ]
 qed-.
@@ -96,26 +96,26 @@ qed-.
 (* Basic properties *********************************************************)
 
 (* Basic_1: was: drop1_skip_bind *)
-lemma drops_skip: ∀L1,L2,s,des. ⬇*[s, des] L1 ≡ L2 → ∀V1,V2. ⬆*[des] V2 ≡ V1 →
-                  ∀I. ⬇*[s, des + 1] L1.ⓑ{I}V1 ≡ L2.ⓑ{I}V2.
-#L1 #L2 #s #des #H elim H -L1 -L2 -des
+lemma drops_skip: ∀L1,L2,s,cs. ⬇*[s, cs] L1 ≡ L2 → ∀V1,V2. ⬆*[cs] V2 ≡ V1 →
+                  ∀I. ⬇*[s, cs + 1] L1.ⓑ{I}V1 ≡ L2.ⓑ{I}V2.
+#L1 #L2 #s #cs #H elim H -L1 -L2 -cs
 [ #L #V1 #V2 #HV12 #I
   >(lifts_inv_nil … HV12) -HV12 //
-| #L1 #L #L2 #des #l #m #_ #HL2 #IHL #V1 #V2 #H #I
+| #L1 #L #L2 #cs #l #m #_ #HL2 #IHL #V1 #V2 #H #I
   elim (lifts_inv_cons … H) -H /3 width=5 by drop_skip, drops_cons/
 ].
 qed.
 
 lemma d1_liftable_liftables: ∀R,s. d_liftable1 R s → d_liftables1 R s.
-#R #s #HR #L #K #des #H elim H -L -K -des
+#R #s #HR #L #K #cs #H elim H -L -K -cs
 [ #L #T #U #H #HT <(lifts_inv_nil … H) -H //
-| #L1 #L #L2 #des #l #m #_ #HL2 #IHL #T2 #T1 #H #HLT2
+| #L1 #L #L2 #cs #l #m #_ #HL2 #IHL #T2 #T1 #H #HLT2
   elim (lifts_inv_cons … H) -H /3 width=10 by/
 ]
 qed.
 
 lemma d1_liftables_liftables_all: ∀R,s. d_liftables1 R s → d_liftables1_all R s.
-#R #s #HR #L #K #des #HLK #Ts #Us #H elim H -Ts -Us normalize //
+#R #s #HR #L #K #cs #HLK #Ts #Us #H elim H -Ts -Us normalize //
 #Ts #Us #T #U #HTU #_ #IHTUs * /3 width=7 by conj/
 qed.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/drops_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/drops_drop.ma
index e835b2e18..2f9a34c08 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/drops_drop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/drops_drop.ma
@@ -19,12 +19,12 @@ include "basic_2/multiple/drops.ma".
 
 (* Properties concerning basic local environment slicing ********************)
 
-lemma drops_drop_trans: ∀L1,L,des. ⬇*[Ⓕ, des] L1 ≡ L → ∀L2,i. ⬇[i] L ≡ L2 →
-                        ∃∃L0,des0,i0. ⬇[i0] L1 ≡ L0 & ⬇*[Ⓕ, des0] L0 ≡ L2 &
-                                      @⦃i, des⦄ ≡ i0 & des ▭ i ≡ des0.
-#L1 #L #des #H elim H -L1 -L -des
+lemma drops_drop_trans: ∀L1,L,cs. ⬇*[Ⓕ, cs] L1 ≡ L → ∀L2,i. ⬇[i] L ≡ L2 →
+                        ∃∃L0,cs0,i0. ⬇[i0] L1 ≡ L0 & ⬇*[Ⓕ, cs0] L0 ≡ L2 &
+                                      @⦃i, cs⦄ ≡ i0 & cs ▭ i ≡ cs0.
+#L1 #L #cs #H elim H -L1 -L -cs
 [ /2 width=7 by drops_nil, minuss_nil, at_nil, ex4_3_intro/
-| #L1 #L0 #L #des #l #m #_ #HL0 #IHL0 #L2 #i #HL2
+| #L1 #L0 #L #cs #l #m #_ #HL0 #IHL0 #L2 #i #HL2
   elim (lt_or_ge i l) #Hil
   [ elim (drop_trans_le … HL0 … HL2) -L /2 width=2 by lt_to_le/
     #L #HL0 #HL2 elim (IHL0 … HL0) -L0 /3 width=7 by drops_cons, minuss_lt, at_lt, ex4_3_intro/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/drops_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/drops_drops.ma
index 2ee3a07ff..c2b0b30d1 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/drops_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/drops_drops.ma
@@ -19,7 +19,7 @@ include "basic_2/multiple/drops_drop.ma".
 (* Main properties **********************************************************)
 
 (* Basic_1: was: drop1_trans *)
-theorem drops_trans: ∀L,L2,s,des2. ⬇*[s, des2] L ≡ L2 → ∀L1,des1. ⬇*[s, des1] L1 ≡ L →
-                     ⬇*[s, des2 @@ des1] L1 ≡ L2.
-#L #L2 #s #des2 #H elim H -L -L2 -des2 /3 width=3 by drops_cons/
+theorem drops_trans: ∀L,L2,s,cs2. ⬇*[s, cs2] L ≡ L2 → ∀L1,cs1. ⬇*[s, cs1] L1 ≡ L →
+                     ⬇*[s, cs2 @@ cs1] L1 ≡ L2.
+#L #L2 #s #cs2 #H elim H -L -L2 -cs2 /3 width=3 by drops_cons/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/fqup.ma
index 6c1e0f127..b126081ba 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/fqup.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/fqup.ma
@@ -98,12 +98,12 @@ lemma fqup_wf_ind: ∀R:relation3 …. (
                       ∀G1,L1,T1. (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → R G2 L2 T2) →
                       R G1 L1 T1
                    ) → ∀G1,L1,T1. R G1 L1 T1.
-#R #HR @(f3_ind … fw) #n #IHn #G1 #L1 #T1 #H destruct /4 width=1 by fqup_fwd_fw/
+#R #HR @(f3_ind … fw) #x #IHx #G1 #L1 #T1 #H destruct /4 width=1 by fqup_fwd_fw/
 qed-.
 
 lemma fqup_wf_ind_eq: ∀R:relation3 …. (
                          ∀G1,L1,T1. (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → R G2 L2 T2) →
                          ∀G2,L2,T2. G1 = G2 → L1 = L2 → T1 = T2 → R G2 L2 T2
                       ) → ∀G1,L1,T1. R G1 L1 T1.
-#R #HR @(f3_ind … fw) #n #IHn #G1 #L1 #T1 #H destruct /4 width=7 by fqup_fwd_fw/
+#R #HR @(f3_ind … fw) #x #IHx #G1 #L1 #T1 #H destruct /4 width=7 by fqup_fwd_fw/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_lift.ma
index 0b60f7af7..a95f1ac3f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_lift.ma
@@ -21,31 +21,31 @@ include "basic_2/multiple/frees.ma".
 
 lemma frees_dec: ∀L,U,l,i. Decidable (frees l L U i).
 #L #U @(f2_ind … rfw … L U) -L -U
-#n #IH #L * *
+#x #IH #L * *
 [ -IH /3 width=5 by frees_inv_sort, or_intror/
-| #j #Hn #l #i elim (lt_or_eq_or_gt i j) #Hji
-  [ -n @or_intror #H elim (lt_refl_false i)
+| #j #Hx #l #i elim (lt_or_eq_or_gt i j) #Hji
+  [ -x @or_intror #H elim (lt_refl_false i)
     lapply (frees_inv_lref_ge … H ?) -L -l /2 width=1 by lt_to_le/
-  | -n /2 width=1 by or_introl/
+  | -x /2 width=1 by or_introl/
   | elim (ylt_split j l) #Hli
-    [ -n @or_intror #H elim (lt_refl_false i)
+    [ -x @or_intror #H elim (lt_refl_false i)
       lapply (frees_inv_lref_skip … H ?) -L //
     | elim (lt_or_ge j (|L|)) #Hj
       [ elim (drop_O1_lt (Ⓕ) L j) // -Hj #I #K #W #HLK destruct
         elim (IH K W … 0 (i-j-1)) -IH [1,3: /3 width=5 by frees_lref_be, drop_fwd_rfw, or_introl/ ] #HnW
         @or_intror #H elim (frees_inv_lref_lt … H) // #Z #Y #X #_ #HLY -l
         lapply (drop_mono … HLY … HLK) -L #H destruct /2 width=1 by/  
-      | -n @or_intror #H elim (lt_refl_false i)
+      | -x @or_intror #H elim (lt_refl_false i)
         lapply (frees_inv_lref_free … H ?) -l //
       ]
     ]
   ]
 | -IH /3 width=5 by frees_inv_gref, or_intror/
-| #a #I #W #U #Hn #l #i destruct
+| #a #I #W #U #Hx #l #i destruct
   elim (IH L W … l i) [1,3: /3 width=1 by frees_bind_sn, or_introl/ ] #HnW
   elim (IH (L.ⓑ{I}W) U … (⫯l) (i+1)) -IH [1,3: /3 width=1 by frees_bind_dx, or_introl/ ] #HnU
   @or_intror #H elim (frees_inv_bind … H) -H /2 width=1 by/
-| #I #W #U #Hn #l #i destruct
+| #I #W #U #Hx #l #i destruct
   elim (IH L W … l i) [1,3: /3 width=1 by frees_flat_sn, or_introl/ ] #HnW
   elim (IH L U … l i) -IH [1,3: /3 width=1 by frees_flat_dx, or_introl/ ] #HnU
   @or_intror #H elim (frees_inv_flat … H) -H /2 width=1 by/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.ma
index d4a5a61cc..be2d50f1e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.ma
@@ -20,75 +20,75 @@ include "basic_2/multiple/mr2_plus.ma".
 
 inductive lifts: list2 nat nat → relation term ≝
 | lifts_nil : ∀T. lifts (◊) T T
-| lifts_cons: ∀T1,T,T2,des,l,m.
-              ⬆[l,m] T1 ≡ T → lifts des T T2 → lifts ({l, m} @ des) T1 T2
+| 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 des T1 T2 = (lifts des T1 T2).
+   'RLiftStar cs T1 T2 = (lifts cs T1 T2).
 
 (* Basic inversion lemmas ***************************************************)
 
-fact lifts_inv_nil_aux: ∀T1,T2,des. ⬆*[des] T1 ≡ T2 → des = ◊ → T1 = T2.
-#T1 #T2 #des * -T1 -T2 -des //
-#T1 #T #T2 #l #m #des #_ #_ #H destruct
+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,des. ⬆*[des] T1 ≡ T2 →
-                         ∀l,m,tl. des = {l, m} @ tl →
+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 #des * -T1 -T2 -des
+#T1 #T2 #cs * -T1 -T2 -cs
 [ #T #l #m #tl #H destruct
-| #T1 #T #T2 #des #l #m #HT1 #HT2 #l0 #m0 #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,des. ⬆*[{l, m} @ des] T1 ≡ T2 →
-                      ∃∃T. ⬆[l, m] T1 ≡ T & ⬆*[des] T ≡ T2.
+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,des. ⬆*[des] ⋆k ≡ T2 → T2 = ⋆k.
-#T2 #k #des elim des -des
+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 #des #IH #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,des,i1. ⬆*[des] #i1 ≡ T2 →
-                       ∃∃i2. @⦃i1, des⦄ ≡ i2 & T2 = #i2.
-#T2 #des elim des -des
+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 #des #IH #i1 #H
+| #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,des. ⬆*[des] §p ≡ T2 → T2 = §p.
-#T2 #p #des elim des -des
+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 #des #IH #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,des,V1,U1. ⬆*[des] ⓑ{a,I} V1. U1 ≡ T2 →
-                       ∃∃V2,U2. ⬆*[des] V1 ≡ V2 & ⬆*[des + 1] U1 ≡ U2 &
+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 #des elim des -des
+#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 #des #IHcs #V1 #U1 #H
+| #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
@@ -97,13 +97,13 @@ lemma lifts_inv_bind1: ∀a,I,T2,des,V1,U1. ⬆*[des] ⓑ{a,I} V1. U1 ≡ T2 →
 qed-.
 
 (* Basic_1: was: lift1_flat *)
-lemma lifts_inv_flat1: ∀I,T2,des,V1,U1. ⬆*[des] ⓕ{I} V1. U1 ≡ T2 →
-                       ∃∃V2,U2. ⬆*[des] V1 ≡ V2 & ⬆*[des] U1 ≡ U2 &
+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 #des elim des -des
+#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 #des #IHcs #V1 #U1 #H
+| #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
@@ -113,38 +113,38 @@ qed-.
 
 (* Basic forward lemmas *****************************************************)
 
-lemma lifts_simple_dx: ∀T1,T2,des. ⬆*[des] T1 ≡ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄.
-#T1 #T2 #des #H elim H -T1 -T2 -des /3 width=5 by lift_simple_dx/
+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,des. ⬆*[des] T1 ≡ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄.
-#T1 #T2 #des #H elim H -T1 -T2 -des /3 width=5 by lift_simple_sn/
+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,des. ⬆*[des] V1 ≡ V2 →
-                  ∀T1. ⬆*[des + 1] T1 ≡ T2 →
-                  ⬆*[des] ⓑ{a,I} V1. T1 ≡ ⓑ{a,I} V2. T2.
-#a #I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des
+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 #des #l #m #HV1 #_ #IHV #T1 #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,des. ⬆*[des] V1 ≡ V2 →
-                  ∀T1. ⬆*[des] T1 ≡ T2 →
-                  ⬆*[des] ⓕ{I} V1. T1 ≡ ⓕ{I} V2. T2.
-#I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des
+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 #des #l #m #HV1 #_ #IHV #T1 #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: ∀des,T1. ∃T2. ⬆*[des] T1 ≡ T2.
-#des elim des -des /2 width=2 by lifts_nil, ex_intro/
-#l #m #des #IH #T1 elim (lift_total T1 l m)
+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
index 990878bee..102ed0ceb 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lift.ma
@@ -21,39 +21,39 @@ include "basic_2/multiple/lifts.ma".
 (* Properties concerning basic term relocation ******************************)
 
 (* Basic_1: was: lift1_xhg (right to left) *)
-lemma lifts_lift_trans_le: ∀T1,T,des. ⬆*[des] T1 ≡ T → ∀T2. ⬆[0, 1] T ≡ T2 →
-                           ∃∃T0. ⬆[0, 1] T1 ≡ T0 & ⬆*[des + 1] T0 ≡ T2.
-#T1 #T #des #H elim H -T1 -T -des
-[ /2 width=3/
-| #T1 #T3 #T #des #l #m #HT13 #_ #IHT13 #T2 #HT2
+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/
+  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: ∀des,i,i0. @⦃i, des⦄ ≡ i0 →
-                        ∀des0. des + 1 ▭ i + 1 ≡ des0 + 1 →
-                        ∀T1,T0. ⬆*[des0] T1 ≡ T0 →
+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 & ⬆*[des] T ≡ T2.
-#des elim des -des normalize
-[ #i #x #H1 #des0 #H2 #T1 #T0 #HT10 #T2
+                        ∃∃T. ⬆[0, i + 1] T1 ≡ T & ⬆*[cs] T ≡ T2.
+#cs elim cs -cs normalize
+[ #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; -des0 #H
-  >(lifts_inv_nil … H) -T1 /2 width=3/
-| #l #m #des #IHcs #i #i0 #H1 #des0 #H2 #T1 #T0 #HT10 #T2 #HT02
+  >(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: /2 width=1/ ] #des1 #Hcs1 <minus_le_minus_minus_comm // <minus_plus_m_m #H
-    elim (pluss_inv_cons2 … H) -H #des2 #H1 #H2 destruct
+  [ elim (minuss_inv_cons1_lt … H2) -H2 [2: /2 width=1 by lt_minus_to_plus/ ] #cs1 #Hcs1 <minus_le_minus_minus_comm // <minus_plus_m_m #H
+    elim (pluss_inv_cons2 … H) -H #cs2 #H1 #H2 destruct
     elim (lifts_inv_cons … HT10) -HT10 #T >minus_plus #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/ #T #HT1 <plus_minus_m_m /2 width=1/ /3 width=5/
+    elim (lift_trans_le … HT1 … HT0) -T /2 width=1 by/ #T #HT1 <plus_minus_m_m /3 width=5 by lifts_cons, ex2_intro/
   | >commutative_plus in Hi0; #Hi0
-    lapply (minuss_inv_cons1_ge … H2 ?) -H2 [ /2 width=1/ ] <associative_plus #Hcs0
+    lapply (minuss_inv_cons1_ge … H2 ?) -H2 [ /2 width=1 by le_S_S/ ] <associative_plus #Hcs0
     elim (IHcs … Hi0 … Hcs0 … HT10 … HT02) -IHcs -Hi0 -Hcs0 -T0 #T0 #HT0 #HT02
-    elim (lift_split … HT0 l (i+1)) -HT0 /2 width=1/ /3 width=5/
+    elim (lift_split … HT0 l (i+1)) -HT0 /3 width=5 by lifts_cons, le_S, ex2_intro/
   ]
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lift_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lift_vector.ma
index ecba0fd77..e09e0f00a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lift_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lift_vector.ma
@@ -21,15 +21,15 @@ include "basic_2/multiple/lifts_vector.ma".
 (* Main properties **********************************************************)
 
 (* Basic_1: was: lifts1_xhg (right to left) *)
-lemma liftsv_liftv_trans_le: ∀T1s,Ts,des. ⬆*[des] T1s ≡ Ts →
+lemma liftsv_liftv_trans_le: ∀T1s,Ts,cs. ⬆*[cs] T1s ≡ Ts →
                              ∀T2s:list term. ⬆[0, 1] Ts ≡ T2s →
-                             ∃∃T0s. ⬆[0, 1] T1s ≡ T0s & ⬆*[des + 1] T0s ≡ T2s.
-#T1s #Ts #des #H elim H -T1s -Ts
+                             ∃∃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/
+  >(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/
+  elim (lifts_lift_trans_le … HT1 … HT2) -T /3 width=5 by liftsv_cons, liftv_cons, ex2_intro/
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lifts.ma
index 739f79009..cff6bf238 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lifts.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lifts.ma
@@ -19,7 +19,7 @@ include "basic_2/multiple/lifts_lift.ma".
 (* Main properties **********************************************************)
 
 (* Basic_1: was: lift1_lift1 (left to right) *)
-theorem lifts_trans: ∀T1,T,des1. ⬆*[des1] T1 ≡ T → ∀T2:term. ∀des2. ⬆*[des2] T ≡ T2 →
-                     ⬆*[des1 @@ des2] T1 ≡ T2.
-#T1 #T #des1 #H elim H -T1 -T -des1 // /3 width=3/
+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.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_vector.ma
index c285d520a..5951134f6 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_vector.ma
@@ -17,26 +17,26 @@ include "basic_2/multiple/lifts.ma".
 
 (* GENERIC TERM VECTOR RELOCATION *******************************************)
 
-inductive liftsv (des:list2 nat nat) : relation (list term) ≝
-| liftsv_nil : liftsv des (◊) (◊)
+inductive liftsv (cs:list2 nat nat) : relation (list term) ≝
+| liftsv_nil : liftsv cs (◊) (◊)
 | liftsv_cons: ∀T1s,T2s,T1,T2.
-               ⬆*[des] T1 ≡ T2 → liftsv des T1s T2s →
-               liftsv des (T1 @ T1s) (T2 @ T2s)
+               ⬆*[cs] T1 ≡ T2 → liftsv cs T1s T2s →
+               liftsv cs (T1 @ T1s) (T2 @ T2s)
 .
 
 interpretation "generic relocation (vector)"
-   'RLiftStar des T1s T2s = (liftsv des T1s T2s).
+   '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,des. ⬆*[des] Ⓐ V1s. U1 ≡ T2 →
-                        ∃∃V2s,U2. ⬆*[des] V1s ≡ V2s & ⬆*[des] U1 ≡ U2 &
+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 #des #HT12  
+[ #T1 #T2 #cs #HT12  
   @ex3_2_intro [3,4: // |1,2: skip | // ] (**) (* explicit constructor *)
-| #V1 #V1s #IHV1s #T1 #X #des #H
+| #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 *)
@@ -46,8 +46,8 @@ qed-.
 (* Basic properties *********************************************************)
 
 (* Basic_1: was: lifts1_flat (right to left) *)
-lemma lifts_applv: ∀V1s,V2s,des. ⬆*[des] V1s ≡ V2s →
-                   ∀T1,T2. ⬆*[des] T1 ≡ T2 →
-                   ⬆*[des] Ⓐ V1s. T1 ≡ Ⓐ V2s. T2.
-#V1s #V2s #des #H elim H -V1s -V2s /3 width=1 by lifts_flat/
+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/lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq.ma
index c9cd4c54c..1f57f73be 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq.ma
@@ -74,7 +74,7 @@ lemma lleq_fwd_lref: ∀L1,L2,l,i. L1 ≡[#i, l] L2 →
                       | ∃∃I,K1,K2,V. ⬇[i] L1 ≡ K1.ⓑ{I}V &
                                      ⬇[i] L2 ≡ K2.ⓑ{I}V &
                                       K1 ≡[V, yinj 0] K2 & l ≤ yinj i.
-#L1 #L2 #l #i #H elim (llpx_sn_fwd_lref … H) /2 width=1/
+#L1 #L2 #l #i #H elim (llpx_sn_fwd_lref … H) /2 width=1 by or3_intro0, or3_intro1/
 * /3 width=7 by or3_intro2, ex4_4_intro/
 qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn.ma
index f75d1a4a9..d95462070 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn.ma
@@ -149,17 +149,17 @@ qed-.
 
 lemma llpx_sn_refl: ∀R. (∀L. reflexive … (R L)) → ∀T,L,l. llpx_sn R l T L L.
 #R #HR #T #L @(f2_ind … rfw … L T) -L -T
-#n #IH #L * * /3 width=1 by llpx_sn_sort, llpx_sn_gref, llpx_sn_bind, llpx_sn_flat/
-#i #Hn elim (lt_or_ge i (|L|)) /2 width=1 by llpx_sn_free/
+#x #IH #L * * /3 width=1 by llpx_sn_sort, llpx_sn_gref, llpx_sn_bind, llpx_sn_flat/
+#i #Hx elim (lt_or_ge i (|L|)) /2 width=1 by llpx_sn_free/
 #HiL #l elim (ylt_split i l) /2 width=1 by llpx_sn_skip/
 elim (drop_O1_lt … HiL) -HiL destruct /4 width=9 by llpx_sn_lref, drop_fwd_rfw/
 qed-.
 
 lemma llpx_sn_Y: ∀R,T,L1,L2. |L1| = |L2| → llpx_sn R (∞) T L1 L2.
 #R #T #L1 @(f2_ind … rfw … L1 T) -L1 -T
-#n #IH #L1 * * /3 width=1 by llpx_sn_sort, llpx_sn_skip, llpx_sn_gref, llpx_sn_flat/
-#a #I #V1 #T1 #Hn #L2 #HL12
-@llpx_sn_bind /2 width=1/ (**) (* explicit constructor *)
+#x #IH #L1 * * /3 width=1 by llpx_sn_sort, llpx_sn_skip, llpx_sn_gref, llpx_sn_flat/
+#a #I #V1 #T1 #Hx #L2 #HL12
+@llpx_sn_bind /2 width=1 by/ (**) (* explicit constructor *)
 @IH -IH // normalize /2 width=1 by eq_f2/
 qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_alt.ma
index ee49dc20c..a849ade55 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_alt.ma
@@ -29,27 +29,27 @@ definition llpx_sn_alt: relation3 lenv term term → relation4 ynat term lenv le
 
 theorem llpx_sn_llpx_sn_alt: ∀R,T,L1,L2,l. llpx_sn R l T L1 L2 → llpx_sn_alt R l T L1 L2.
 #R #U #L1 @(f2_ind … rfw … L1 U) -L1 -U
-#n #IHn #L1 #U #Hn #L2 #l #H elim (llpx_sn_inv_alt_r … H) -H
+#x #IHx #L1 #U #Hx #L2 #l #H elim (llpx_sn_inv_alt_r … H) -H
 #HL12 #IHU @conj //
 #I1 #I2 #K1 #K2 #V1 #V2 #i #Hli #H #HLK1 #HLK2 elim (frees_inv … H) -H
-[ -n #HnU elim (IHU … HnU HLK1 HLK2) -IHU -HnU -HLK1 -HLK2 /2 width=1 by conj/
+[ -x #HnU elim (IHU … HnU HLK1 HLK2) -IHU -HnU -HLK1 -HLK2 /2 width=1 by conj/
 | * #J1 #K10 #W10 #j #Hlj #Hji #HnU #HLK10 #HnW10 destruct
   lapply (drop_fwd_drop2 … HLK10) #H
   lapply (drop_conf_ge … H … HLK1 ?) -H /2 width=1 by lt_to_le/ <minus_plus #HK10
   elim (drop_O1_lt (Ⓕ) L2 j) [2: <HL12 /2 width=5 by drop_fwd_length_lt2/ ] #J2 #K20 #W20 #HLK20
   lapply (drop_fwd_drop2 … HLK20) #H
   lapply (drop_conf_ge … H … HLK2 ?) -H /2 width=1 by lt_to_le/ <minus_plus #HK20
-  elim (IHn K10 W10 … K20 0) -IHn -HL12 /3 width=6 by drop_fwd_rfw/
+  elim (IHx K10 W10 … K20 0) -IHx -HL12 /3 width=6 by drop_fwd_rfw/
   elim (IHU … HnU HLK10 HLK20) -IHU -HnU -HLK10 -HLK20 //
 ]
 qed.
 
 theorem llpx_sn_alt_inv_llpx_sn: ∀R,T,L1,L2,l. llpx_sn_alt R l T L1 L2 → llpx_sn R l T L1 L2.
 #R #U #L1 @(f2_ind … rfw … L1 U) -L1 -U
-#n #IHn #L1 #U #Hn #L2 #l * #HL12 #IHU @llpx_sn_intro_alt_r //
+#x #IHx #L1 #U #Hx #L2 #l * #HL12 #IHU @llpx_sn_intro_alt_r //
 #I1 #I2 #K1 #K2 #V1 #V2 #i #Hli #HnU #HLK1 #HLK2 destruct
 elim (IHU … HLK1 HLK2) /3 width=2 by frees_eq/
-#H #HV12 @and3_intro // @IHn -IHn /3 width=6 by drop_fwd_rfw/
+#H #HV12 @and3_intro // @IHx -IHx /3 width=6 by drop_fwd_rfw/
 lapply (drop_fwd_drop2 … HLK1) #H1
 lapply (drop_fwd_drop2 … HLK2) -HLK2 #H2
 @conj [ @(drop_fwd_length_eq1 … H1 H2) // ] -HL12
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_alt_rec.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_alt_rec.ma
index 0f38faaa8..6cd1b9bd9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_alt_rec.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_alt_rec.ma
@@ -195,17 +195,17 @@ qed.
 (* Main inversion lemmas ****************************************************)
 
 theorem llpx_sn_alt_r_inv_lpx_sn: ∀R,T,L1,L2,l. llpx_sn_alt_r R l T L1 L2 → llpx_sn R l T L1 L2.
-#R #T #L1 @(f2_ind … rfw … L1 T) -L1 -T #n #IH #L1 * *
+#R #T #L1 @(f2_ind … rfw … L1 T) -L1 -T #x #IH #L1 * *
 [1,3: /3 width=4 by llpx_sn_alt_r_fwd_length, llpx_sn_gref, llpx_sn_sort/
-| #i #Hn #L2 #l #H lapply (llpx_sn_alt_r_fwd_length … H)
+| #i #Hx #L2 #l #H lapply (llpx_sn_alt_r_fwd_length … H)
   #HL12 elim (llpx_sn_alt_r_fwd_lref … H) -H
   [ * /2 width=1 by llpx_sn_free/
   | /2 width=1 by llpx_sn_skip/
   | * /4 width=9 by llpx_sn_lref, drop_fwd_rfw/
   ]
-| #a #I #V #T #Hn #L2 #l #H elim (llpx_sn_alt_r_inv_bind … H) -H
+| #a #I #V #T #Hx #L2 #l #H elim (llpx_sn_alt_r_inv_bind … H) -H
   /3 width=1 by llpx_sn_bind/
-| #I #V #T #Hn #L2 #l #H elim (llpx_sn_alt_r_inv_flat … H) -H
+| #I #V #T #Hx #L2 #l #H elim (llpx_sn_alt_r_inv_flat … H) -H
   /3 width=1 by llpx_sn_flat/
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_drop.ma
index de36874c9..12d7e325c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_drop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_drop.ma
@@ -128,9 +128,9 @@ lemma llpx_sn_bind_repl_O: ∀R,I,L1,L2,V1,V2,T. llpx_sn R 0 T (L1.ⓑ{I}V1) (L2
 lemma llpx_sn_dec: ∀R. (∀L,T1,T2. Decidable (R L T1 T2)) →
                    ∀T,L1,L2,l. Decidable (llpx_sn R l T L1 L2).
 #R #HR #T #L1 @(f2_ind … rfw … L1 T) -L1 -T
-#n #IH #L1 * *
-[ #k #Hn #L2 elim (eq_nat_dec (|L1|) (|L2|)) /3 width=1 by or_introl, llpx_sn_sort/
-| #i #Hn #L2 elim (eq_nat_dec (|L1|) (|L2|))
+#x #IH #L1 * *
+[ #k #Hx #L2 elim (eq_nat_dec (|L1|) (|L2|)) /3 width=1 by or_introl, llpx_sn_sort/
+| #i #Hx #L2 elim (eq_nat_dec (|L1|) (|L2|))
   [ #HL12 #l elim (ylt_split i l) /3 width=1 by llpx_sn_skip, or_introl/
     #Hli elim (lt_or_ge i (|L1|)) #HiL1
     elim (lt_or_ge i (|L2|)) #HiL2 /3 width=1 by or_introl, llpx_sn_free/
@@ -152,19 +152,19 @@ lemma llpx_sn_dec: ∀R. (∀L,T1,T2. Decidable (R L T1 T2)) →
     lapply (drop_mono … HLY2 … HLK2) -HLY2 -HLK2
     #H #H0 destruct /2 width=1 by/
   ]
-| #p #Hn #L2 elim (eq_nat_dec (|L1|) (|L2|)) /3 width=1 by or_introl, llpx_sn_gref/
-| #a #I #V #T #Hn #L2 #l destruct
+| #p #Hx #L2 elim (eq_nat_dec (|L1|) (|L2|)) /3 width=1 by or_introl, llpx_sn_gref/
+| #a #I #V #T #Hx #L2 #l destruct
   elim (IH L1 V … L2 l) /2 width=1 by/
   elim (IH (L1.ⓑ{I}V) T … (L2.ⓑ{I}V) (⫯l)) -IH /3 width=1 by or_introl, llpx_sn_bind/
   #H1 #H2 @or_intror
   #H elim (llpx_sn_inv_bind … H) -H /2 width=1 by/
-| #I #V #T #Hn #L2 #l destruct
+| #I #V #T #Hx #L2 #l destruct
   elim (IH L1 V … L2 l) /2 width=1 by/
   elim (IH L1 T … L2 l) -IH /3 width=1 by or_introl, llpx_sn_flat/
   #H1 #H2 @or_intror
   #H elim (llpx_sn_inv_flat … H) -H /2 width=1 by/
 ]
--n /4 width=4 by llpx_sn_fwd_length, or_intror/
+-x /4 width=4 by llpx_sn_fwd_length, or_intror/
 qed-.
 
 (* Properties on relocation *************************************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_lpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_lpx_sn.ma
index b4b7f7ebe..a66b866f4 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_lpx_sn.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_lpx_sn.ma
@@ -22,12 +22,12 @@ include "basic_2/multiple/llpx_sn.ma".
 lemma lpx_sn_llpx_sn: ∀R. (∀L. reflexive … (R L)) →
                       ∀T,L1,L2,l. lpx_sn R L1 L2 → llpx_sn R l T L1 L2.
 #R #HR #T #L1 @(f2_ind … rfw … L1 T) -L1 -T
-#n #IH #L1 * *
+#x #IH #L1 * *
 [ -HR -IH /4 width=2 by lpx_sn_fwd_length, llpx_sn_sort/
 | -HR #i elim (lt_or_ge i (|L1|))
   [2: -IH /4 width=4 by lpx_sn_fwd_length, llpx_sn_free, le_repl_sn_conf_aux/ ]
-  #Hi #Hn #L2 #l elim (ylt_split i l) 
-  [ -n /3 width=2 by llpx_sn_skip, lpx_sn_fwd_length/ ]
+  #Hi #Hx #L2 #l elim (ylt_split i l) 
+  [ -x /3 width=2 by llpx_sn_skip, lpx_sn_fwd_length/ ]
   #Hli #HL12 elim (drop_O1_lt (Ⓕ) L1 i) //
   #I #K1 #V1 #HLK1 elim (lpx_sn_drop_conf … HL12 … HLK1) -HL12
   /4 width=9 by llpx_sn_lref, drop_fwd_rfw/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2.ma
index 9691de8a2..6b5684072 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2.ma
@@ -19,55 +19,55 @@ include "basic_2/grammar/term_vector.ma".
 
 inductive at: list2 nat nat → relation nat ≝
 | at_nil: ∀i. at (◊) i i
-| at_lt : ∀des,l,m,i1,i2. i1 < l →
-          at des i1 i2 → at ({l, m} @ des) i1 i2
-| at_ge : ∀des,l,m,i1,i2. l ≤ i1 →
-          at des (i1 + m) i2 → at ({l, m} @ des) i1 i2
+| at_lt : ∀cs,l,m,i1,i2. i1 < l →
+          at cs i1 i2 → at ({l, m} @ cs) i1 i2
+| at_ge : ∀cs,l,m,i1,i2. l ≤ i1 →
+          at cs (i1 + m) i2 → at ({l, m} @ cs) i1 i2
 .
 
 interpretation "application (multiple relocation with pairs)"
-   'RAt i1 des i2 = (at des i1 i2).
+   'RAt i1 cs i2 = (at cs i1 i2).
 
 (* Basic inversion lemmas ***************************************************)
 
-fact at_inv_nil_aux: ∀des,i1,i2. @⦃i1, des⦄ ≡ i2 → des = ◊ → i1 = i2.
-#des #i1 #i2 * -des -i1 -i2
+fact at_inv_nil_aux: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → cs = ◊ → i1 = i2.
+#cs #i1 #i2 * -cs -i1 -i2
 [ //
-| #des #l #m #i1 #i2 #_ #_ #H destruct
-| #des #l #m #i1 #i2 #_ #_ #H destruct
+| #cs #l #m #i1 #i2 #_ #_ #H destruct
+| #cs #l #m #i1 #i2 #_ #_ #H destruct
 ]
 qed-.
 
 lemma at_inv_nil: ∀i1,i2. @⦃i1, ◊⦄ ≡ i2 → i1 = i2.
 /2 width=3 by at_inv_nil_aux/ qed-.
 
-fact at_inv_cons_aux: ∀des,i1,i2. @⦃i1, des⦄ ≡ i2 →
-                      ∀l,m,des0. des = {l, m} @ des0 →
-                      i1 < l ∧ @⦃i1, des0⦄ ≡ i2 ∨
-                      l ≤ i1 ∧ @⦃i1 + m, des0⦄ ≡ i2.
-#des #i1 #i2 * -des -i1 -i2
-[ #i #l #m #des #H destruct
-| #des1 #l1 #m1 #i1 #i2 #Hil1 #Hi12 #l2 #m2 #des2 #H destruct /3 width=1 by or_introl, conj/
-| #des1 #l1 #m1 #i1 #i2 #Hli1 #Hi12 #l2 #m2 #des2 #H destruct /3 width=1 by or_intror, conj/
+fact at_inv_cons_aux: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 →
+                      ∀l,m,cs0. cs = {l, m} @ cs0 →
+                      i1 < l ∧ @⦃i1, cs0⦄ ≡ i2 ∨
+                      l ≤ i1 ∧ @⦃i1 + m, cs0⦄ ≡ i2.
+#cs #i1 #i2 * -cs -i1 -i2
+[ #i #l #m #cs #H destruct
+| #cs1 #l1 #m1 #i1 #i2 #Hil1 #Hi12 #l2 #m2 #cs2 #H destruct /3 width=1 by or_introl, conj/
+| #cs1 #l1 #m1 #i1 #i2 #Hli1 #Hi12 #l2 #m2 #cs2 #H destruct /3 width=1 by or_intror, conj/
 ]
 qed-.
 
-lemma at_inv_cons: ∀des,l,m,i1,i2. @⦃i1, {l, m} @ des⦄ ≡ i2 →
-                   i1 < l ∧ @⦃i1, des⦄ ≡ i2 ∨
-                   l ≤ i1 ∧ @⦃i1 + m, des⦄ ≡ i2.
+lemma at_inv_cons: ∀cs,l,m,i1,i2. @⦃i1, {l, m} @ cs⦄ ≡ i2 →
+                   i1 < l ∧ @⦃i1, cs⦄ ≡ i2 ∨
+                   l ≤ i1 ∧ @⦃i1 + m, cs⦄ ≡ i2.
 /2 width=3 by at_inv_cons_aux/ qed-.
 
-lemma at_inv_cons_lt: ∀des,l,m,i1,i2. @⦃i1, {l, m} @ des⦄ ≡ i2 →
-                      i1 < l → @⦃i1, des⦄ ≡ i2.
-#des #l #m #i1 #m2 #H
+lemma at_inv_cons_lt: ∀cs,l,m,i1,i2. @⦃i1, {l, m} @ cs⦄ ≡ i2 →
+                      i1 < l → @⦃i1, cs⦄ ≡ i2.
+#cs #l #m #i1 #m2 #H
 elim (at_inv_cons … H) -H * // #Hli1 #_ #Hi1l
 lapply (le_to_lt_to_lt … Hli1 Hi1l) -Hli1 -Hi1l #Hl
 elim (lt_refl_false … Hl)
 qed-.
 
-lemma at_inv_cons_ge: ∀des,l,m,i1,i2. @⦃i1, {l, m} @ des⦄ ≡ i2 →
-                      l ≤ i1 → @⦃i1 + m, des⦄ ≡ i2.
-#des #l #m #i1 #m2 #H
+lemma at_inv_cons_ge: ∀cs,l,m,i1,i2. @⦃i1, {l, m} @ cs⦄ ≡ i2 →
+                      l ≤ i1 → @⦃i1 + m, cs⦄ ≡ i2.
+#cs #l #m #i1 #m2 #H
 elim (at_inv_cons … H) -H * // #Hi1l #_ #Hli1
 lapply (le_to_lt_to_lt … Hli1 Hi1l) -Hli1 -Hi1l #Hl
 elim (lt_refl_false … Hl)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_minus.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_minus.ma
index ce2918fdd..ac00f87b3 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_minus.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_minus.ma
@@ -19,58 +19,58 @@ include "basic_2/multiple/mr2.ma".
 
 inductive minuss: nat → relation (list2 nat nat) ≝
 | minuss_nil: ∀i. minuss i (◊) (◊)
-| minuss_lt : ∀des1,des2,l,m,i. i < l → minuss i des1 des2 →
-              minuss i ({l, m} @ des1) ({l - i, m} @ des2)
-| minuss_ge : ∀des1,des2,l,m,i. l ≤ i → minuss (m + i) des1 des2 →
-              minuss i ({l, m} @ des1) des2
+| minuss_lt : ∀cs1,cs2,l,m,i. i < l → minuss i cs1 cs2 →
+              minuss i ({l, m} @ cs1) ({l - i, m} @ cs2)
+| minuss_ge : ∀cs1,cs2,l,m,i. l ≤ i → minuss (m + i) cs1 cs2 →
+              minuss i ({l, m} @ cs1) cs2
 .
 
 interpretation "minus (multiple relocation with pairs)"
-   'RMinus des1 i des2 = (minuss i des1 des2).
+   'RMinus cs1 i cs2 = (minuss i cs1 cs2).
 
 (* Basic inversion lemmas ***************************************************)
 
-fact minuss_inv_nil1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 → des1 = ◊ → des2 = ◊.
-#des1 #des2 #i * -des1 -des2 -i
+fact minuss_inv_nil1_aux: ∀cs1,cs2,i. cs1 ▭ i ≡ cs2 → cs1 = ◊ → cs2 = ◊.
+#cs1 #cs2 #i * -cs1 -cs2 -i
 [ //
-| #des1 #des2 #l #m #i #_ #_ #H destruct
-| #des1 #des2 #l #m #i #_ #_ #H destruct
+| #cs1 #cs2 #l #m #i #_ #_ #H destruct
+| #cs1 #cs2 #l #m #i #_ #_ #H destruct
 ]
 qed-.
 
-lemma minuss_inv_nil1: ∀des2,i. ◊ ▭ i ≡ des2 → des2 = ◊.
+lemma minuss_inv_nil1: ∀cs2,i. ◊ ▭ i ≡ cs2 → cs2 = ◊.
 /2 width=4 by minuss_inv_nil1_aux/ qed-.
 
-fact minuss_inv_cons1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 →
-                           ∀l,m,des. des1 = {l, m} @ des →
-                           l ≤ i ∧ des ▭ m + i ≡ des2 ∨
-                           ∃∃des0. i < l & des ▭ i ≡ des0 &
-                                   des2 = {l - i, m} @ des0.
-#des1 #des2 #i * -des1 -des2 -i
-[ #i #l #m #des #H destruct
-| #des1 #des #l1 #m1 #i1 #Hil1 #Hcs #l2 #m2 #des2 #H destruct /3 width=3 by ex3_intro, or_intror/
-| #des1 #des #l1 #m1 #i1 #Hli1 #Hcs #l2 #m2 #des2 #H destruct /3 width=1 by or_introl, conj/
+fact minuss_inv_cons1_aux: ∀cs1,cs2,i. cs1 ▭ i ≡ cs2 →
+                           ∀l,m,cs. cs1 = {l, m} @ cs →
+                           l ≤ i ∧ cs ▭ m + i ≡ cs2 ∨
+                           ∃∃cs0. i < l & cs ▭ i ≡ cs0 &
+                                   cs2 = {l - i, m} @ cs0.
+#cs1 #cs2 #i * -cs1 -cs2 -i
+[ #i #l #m #cs #H destruct
+| #cs1 #cs #l1 #m1 #i1 #Hil1 #Hcs #l2 #m2 #cs2 #H destruct /3 width=3 by ex3_intro, or_intror/
+| #cs1 #cs #l1 #m1 #i1 #Hli1 #Hcs #l2 #m2 #cs2 #H destruct /3 width=1 by or_introl, conj/
 ]
 qed-.
 
-lemma minuss_inv_cons1: ∀des1,des2,l,m,i. {l, m} @ des1 ▭ i ≡ des2 →
-                        l ≤ i ∧ des1 ▭ m + i ≡ des2 ∨
-                        ∃∃des. i < l & des1 ▭ i ≡ des &
-                               des2 = {l - i, m} @ des.
+lemma minuss_inv_cons1: ∀cs1,cs2,l,m,i. {l, m} @ cs1 ▭ i ≡ cs2 →
+                        l ≤ i ∧ cs1 ▭ m + i ≡ cs2 ∨
+                        ∃∃cs. i < l & cs1 ▭ i ≡ cs &
+                               cs2 = {l - i, m} @ cs.
 /2 width=3 by minuss_inv_cons1_aux/ qed-.
 
-lemma minuss_inv_cons1_ge: ∀des1,des2,l,m,i. {l, m} @ des1 ▭ i ≡ des2 →
-                           l ≤ i → des1 ▭ m + i ≡ des2.
-#des1 #des2 #l #m #i #H
-elim (minuss_inv_cons1 … H) -H * // #des #Hil #_ #_ #Hli
+lemma minuss_inv_cons1_ge: ∀cs1,cs2,l,m,i. {l, m} @ cs1 ▭ i ≡ cs2 →
+                           l ≤ i → cs1 ▭ m + i ≡ cs2.
+#cs1 #cs2 #l #m #i #H
+elim (minuss_inv_cons1 … H) -H * // #cs #Hil #_ #_ #Hli
 lapply (lt_to_le_to_lt … Hil Hli) -Hil -Hli #Hi
 elim (lt_refl_false … Hi)
 qed-.
 
-lemma minuss_inv_cons1_lt: ∀des1,des2,l,m,i. {l, m} @ des1 ▭ i ≡ des2 →
+lemma minuss_inv_cons1_lt: ∀cs1,cs2,l,m,i. {l, m} @ cs1 ▭ i ≡ cs2 →
                            i < l →
-                           ∃∃des. des1 ▭ i ≡ des & des2 = {l - i, m} @ des.
-#des1 #des2 #l #m #i #H elim (minuss_inv_cons1 … H) -H * /2 width=3 by ex2_intro/
+                           ∃∃cs. cs1 ▭ i ≡ cs & cs2 = {l - i, m} @ cs.
+#cs1 #cs2 #l #m #i #H elim (minuss_inv_cons1 … H) -H * /2 width=3 by ex2_intro/
 #Hli #_ #Hil lapply (lt_to_le_to_lt … Hil Hli) -Hil -Hli
 #Hi elim (lt_refl_false … Hi)
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_mr2.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_mr2.ma
index 2126666e3..858773399 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_mr2.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_mr2.ma
@@ -18,12 +18,12 @@ include "basic_2/multiple/mr2.ma".
 
 (* Main properties **********************************************************)
 
-theorem at_mono: ∀des,i,i1. @⦃i, des⦄ ≡ i1 → ∀i2. @⦃i, des⦄ ≡ i2 → i1 = i2.
-#des #i #i1 #H elim H -des -i -i1
+theorem at_mono: ∀cs,i,i1. @⦃i, cs⦄ ≡ i1 → ∀i2. @⦃i, cs⦄ ≡ i2 → i1 = i2.
+#cs #i #i1 #H elim H -cs -i -i1
 [ #i #x #H <(at_inv_nil … H) -x //
-| #des #l #m #i #i1 #Hil #_ #IHi1 #x #H
+| #cs #l #m #i #i1 #Hil #_ #IHi1 #x #H
   lapply (at_inv_cons_lt … H Hil) -H -Hil /2 width=1 by/
-| #des #l #m #i #i1 #Hli #_ #IHi1 #x #H
+| #cs #l #m #i #i1 #Hli #_ #IHi1 #x #H
   lapply (at_inv_cons_ge … H Hli) -H -Hli /2 width=1 by/
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_plus.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_plus.ma
index bedc3dae2..99b2d4b17 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_plus.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_plus.ma
@@ -16,9 +16,9 @@ include "basic_2/multiple/mr2.ma".
 
 (* MULTIPLE RELOCATION WITH PAIRS *******************************************)
 
-let rec pluss (des:list2 nat nat) (i:nat) on des ≝ match des with
+let rec pluss (cs:list2 nat nat) (i:nat) on cs ≝ match cs with
 [ nil2          ⇒ ◊
-| cons2 l m des ⇒ {l + i, m} @ pluss des i
+| cons2 l m cs ⇒ {l + i, m} @ pluss cs i
 ].
 
 interpretation "plus (multiple relocation with pairs)"
@@ -26,15 +26,15 @@ interpretation "plus (multiple relocation with pairs)"
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma pluss_inv_nil2: ∀i,des. des + i = ◊ → des = ◊.
+lemma pluss_inv_nil2: ∀i,cs. cs + i = ◊ → cs = ◊.
 #i * // normalize
-#l #m #des #H destruct
+#l #m #cs #H destruct
 qed.
 
-lemma pluss_inv_cons2: ∀i,l,m,des2,des. des + i = {l, m} @ des2 →
-                       ∃∃des1. des1 + i = des2 & des = {l - i, m} @ des1.
-#i #l #m #des2 * normalize
+lemma pluss_inv_cons2: ∀i,l,m,cs2,cs. cs + i = {l, m} @ cs2 →
+                       ∃∃cs1. cs1 + i = cs2 & cs = {l - i, m} @ cs1.
+#i #l #m #cs2 * normalize
 [ #H destruct
-| #l1 #m1 #des1 #H destruct /2 width=3/
+| #l1 #m1 #cs1 #H destruct /2 width=3 by ex2_intro/
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir.ma
index 576633954..ba5ba7e7e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir.ma
@@ -43,7 +43,7 @@ qed-.
 
 lemma cir_inv_appl: ∀G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐈⦃ⓐV.T⦄ →
                     ∧∧ ⦃G, L⦄ ⊢ ➡ 𝐈⦃V⦄ & ⦃G, L⦄ ⊢ ➡ 𝐈⦃T⦄ & 𝐒⦃T⦄.
-#G #L #V #T #HVT @and3_intro /3 width=1/
+#G #L #V #T #HVT @and3_intro /3 width=1 by crr_appl_sn, crr_appl_dx/
 generalize in match HVT; -HVT elim T -T //
 * // #a * #U #T #_ #_ #H elim H -H /2 width=1 by crr_beta, crr_theta/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma
index e1d75cd04..31291bc3d 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma
@@ -25,16 +25,16 @@ lemma cnr_inv_crr: ∀G,L,T. ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ 
 [ #L #K #V #i #HLK #H
   elim (cnr_inv_delta … HLK H)
 | #L #V #T #_ #IHV #H
-  elim (cnr_inv_appl … H) -H /2 width=1/
+  elim (cnr_inv_appl … H) -H /2 width=1 by/
 | #L #V #T #_ #IHT #H
-  elim (cnr_inv_appl … H) -H /2 width=1/
+  elim (cnr_inv_appl … H) -H /2 width=1 by/
 | #I #L #V #T * #H1 #H2 destruct
   [ elim (cnr_inv_zeta … H2)
   | elim (cnr_inv_eps … H2)
   ]
 |5,6: #a * [ elim a ] #L #V #T * #H1 #_ #IH #H2 destruct
-  [1,3: elim (cnr_inv_abbr … H2) -H2 /2 width=1/
-  |*: elim (cnr_inv_abst … H2) -H2 /2 width=1/
+  [1,3: elim (cnr_inv_abbr … H2) -H2 /2 width=1 by/
+  |*: elim (cnr_inv_abst … H2) -H2 /2 width=1 by/
   ]
 | #a #L #V #W #T #H
   elim (cnr_inv_appl … H) -H #_ #_ #H
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma
index 61d8fd931..6dafc6d8c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma
@@ -264,7 +264,7 @@ lemma cpr_inv_appl1_simple: ∀G,L,V1,T1,U. ⦃G, L⦄ ⊢ ⓐV1. T1 ➡ U → 
                                      U = ⓐV2. T2.
 #G #L #V1 #T1 #U #H #HT1
 elim (cpr_inv_appl1 … H) -H *
-[ /2 width=5/
+[ /2 width=5 by ex3_2_intro/
 | #a #V2 #W1 #W2 #U1 #U2 #_ #_ #_ #H #_ destruct
   elim (simple_inv_bind … HT1)
 | #a #V #V2 #W1 #W2 #U1 #U2 #_ #_ #_ #_ #H #_ destruct
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_cir.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_cir.ma
index 99846d67a..1f2f97e32 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_cir.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_cir.ma
@@ -38,7 +38,7 @@ lemma cpr_fwd_cir: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ ➡
 | #G #L #V1 #T1 #T #T2 #_ #_ #_ #H
   elim (cir_inv_ri2 … H) /2 width=1 by or_introl/
 | #G #L #V1 #T1 #T2 #_ #_ #H
-  elim (cir_inv_ri2 … H) /2 width=1/
+  elim (cir_inv_ri2 … H) /2 width=1 by/
 | #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #H
   elim (cir_inv_appl … H) -H #_ #_ #H
   elim (simple_inv_bind … H)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
index d16ff6b2e..76b7e0411 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
@@ -119,7 +119,7 @@ lemma cpx_inv_lift1: ∀h,g,G. d_deliftable_sn (cpx h g G).
   elim (IHU12 … HLK … HTU1) -U1 -HLK /3 width=5 by cpx_flat, lift_flat, ex2_intro/
 | #G #L #V #U1 #U #U2 #_ #HU2 #IHU1 #K #s #l #m #HLK #X #H
   elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
-  elim (IHU1 (K.ⓓW1) s … HTU1) /2 width=1/ -L -U1 #T #HTU #HT1
+  elim (IHU1 (K.ⓓW1) s … HTU1) /2 width=1 by drop_skip/ -L -U1 #T #HTU #HT1
   elim (lift_div_le … HU2 … HTU) -U /3 width=5 by cpx_zeta, ex2_intro/
 | #G #L #V #U1 #U2 #_ #IHU12 #K #s #l #m #HLK #X #H
   elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma
index 284fafe20..fad8b481a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma
@@ -244,7 +244,7 @@ fact cpr_conf_lpr_beta_beta:
 #a #G #L0 #V0 #W0 #T0 #IH #V1 #HV01 #W1 #HW01 #T1 #HT01
 #V2 #HV02 #W2 #HW02 #T2 #HT02 #L1 #HL01 #L2 #HL02
 elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2
-elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1/ #W #HW1 #HW2
+elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1 by/ #W #HW1 #HW2
 elim (IH … HT01 … HT02 (L1.ⓛW1) … (L2.ⓛW2)) /2 width=1 by lpr_pair/ -L0 -V0 -W0 -T0 #T #HT1 #HT2
 lapply (lsubr_cpr_trans … HT1 (L1.ⓓⓝW1.V1) ?) -HT1 /2 width=1 by lsubr_beta/
 lapply (lsubr_cpr_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1 by lsubr_beta/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_aaa.ma
index 2c6d530db..76bf7e529 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_aaa.ma
@@ -25,15 +25,15 @@ theorem aaa_mono: ∀G,L,T,A1. ⦃G, L⦄ ⊢ T ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢
   >(aaa_inv_sort … H) -H //
 | #I1 #G #L #K1 #V1 #B #i #HLK1 #_ #IHA1 #A2 #H
   elim (aaa_inv_lref … H) -H #I2 #K2 #V2 #HLK2 #HA2
-  lapply (drop_mono … HLK1 … HLK2) -L #H destruct /2 width=1/
+  lapply (drop_mono … HLK1 … HLK2) -L #H destruct /2 width=1 by/
 | #a #G #L #V #T #B1 #A1 #_ #_ #_ #IHA1 #A2 #H
-  elim (aaa_inv_abbr … H) -H /2 width=1/
+  elim (aaa_inv_abbr … H) -H /2 width=1 by/
 | #a #G #L #V1 #T1 #B1 #A1 #_ #_ #IHB1 #IHA1 #X #H
-  elim (aaa_inv_abst … H) -H #B2 #A2 #HB2 #HA2 #H destruct /3 width=1/
+  elim (aaa_inv_abst … H) -H #B2 #A2 #HB2 #HA2 #H destruct /3 width=1 by eq_f2/
 | #G #L #V1 #T1 #B1 #A1 #_ #_ #_ #IHA1 #A2 #H
   elim (aaa_inv_appl … H) -H #B2 #_ #HA2
   lapply (IHA1 … HA2) -L #H destruct //
 | #G #L #V #T #A1 #_ #_ #_ #IHA1 #A2 #H
-  elim (aaa_inv_cast … H) -H /2 width=1/
+  elim (aaa_inv_cast … H) -H /2 width=1 by/
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lifts.ma
index 051ab4d29..cf972d088 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lifts.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lifts.ma
@@ -19,12 +19,12 @@ include "basic_2/static/aaa_lift.ma".
 
 (* Properties concerning generic relocation *********************************)
 
-lemma aaa_lifts: ∀G,L1,L2,T2,A,s,des. ⬇*[s, des] L2 ≡ L1 → ∀T1. ⬆*[des] T1 ≡ T2 →
+lemma aaa_lifts: ∀G,L1,L2,T2,A,s,cs. ⬇*[s, cs] L2 ≡ L1 → ∀T1. ⬆*[cs] T1 ≡ T2 →
                  ⦃G, L1⦄ ⊢ T1 ⁝ A → ⦃G, L2⦄ ⊢ T2 ⁝ A.
-#G #L1 #L2 #T2 #A #s #des #H elim H -L1 -L2 -des
+#G #L1 #L2 #T2 #A #s #cs #H elim H -L1 -L2 -cs
 [ #L #T1 #H #HT1
   <(lifts_inv_nil … H) -H //
-| #L1 #L #L2 #des #l #m #_ #HL2 #IHL1 #T1 #H #HT1
+| #L1 #L #L2 #cs #l #m #_ #HL2 #IHL1 #T1 #H #HT1
   elim (lifts_inv_cons … H) -H /3 width=10 by aaa_lift/
 ]
 qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/da_da.ma b/matita/matita/contribs/lambdadelta/basic_2/static/da_da.ma
index 64b7b7d84..c670e0a5d 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/da_da.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/da_da.ma
@@ -26,13 +26,13 @@ theorem da_mono: ∀h,g,G,L,T,d1. ⦃G, L⦄ ⊢ T ▪[h, g] d1 →
   >(deg_mono … Hkd2 … Hkd1) -h -k -d2 //
 | #G #L #K #V #i #d1 #HLK #_ #IHV #d2 #H
   elim (da_inv_lref … H) -H * #K0 #V0 [| #d0 ] #HLK0 #HV0 [| #Hd0 ]
-  lapply (drop_mono … HLK0 … HLK) -HLK -HLK0 #H destruct /2 width=1/
+  lapply (drop_mono … HLK0 … HLK) -HLK -HLK0 #H destruct /2 width=1 by/
 | #G #L #K #W #i #d1 #HLK #_ #IHW #d2 #H
   elim (da_inv_lref … H) -H * #K0 #W0 [| #d0 ] #HLK0 #HW0 [| #Hd0 ]
-  lapply (drop_mono … HLK0 … HLK) -HLK -HLK0 #H destruct /3 width=1/
+  lapply (drop_mono … HLK0 … HLK) -HLK -HLK0 #H destruct /3 width=1 by eq_f/
 | #a #I #G #L #V #T #d1 #_ #IHT #d2 #H
-  lapply (da_inv_bind … H) -H /2 width=1/
+  lapply (da_inv_bind … H) -H /2 width=1 by/
 | #I #G #L #V #T #d1 #_ #IHT #d2 #H
-  lapply (da_inv_flat … H) -H /2 width=1/
+  lapply (da_inv_flat … H) -H /2 width=1 by/
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_lsuba.ma
index cc4af1670..bb77403bd 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_lsuba.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_lsuba.ma
@@ -23,7 +23,7 @@ theorem lsuba_trans: ∀G,L1,L. G ⊢ L1 ⫃⁝ L → ∀L2. G ⊢ L ⫃⁝ L2 
 [ #X #H >(lsuba_inv_atom1 … H) -H //
 | #I #L1 #L #Y #HL1 #IHL1 #X #H
   elim (lsuba_inv_pair1 … H) -H * #L2
-  [ #HL2 #H destruct /3 width=1/
+  [ #HL2 #H destruct /3 width=1 by lsuba_pair/
   | #W #V #A #HV #HW #HL2 #H1 #H2 #H3 destruct
     /3 width=3 by lsuba_beta, lsuba_aaa_trans/
   ]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubd_da.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubd_da.ma
index 457b64e77..111a0103a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubd_da.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubd_da.ma
@@ -22,44 +22,44 @@ include "basic_2/static/lsubd.ma".
 lemma lsubd_da_trans: ∀h,g,G,L2,T,d. ⦃G, L2⦄ ⊢ T ▪[h, g] d →
                       ∀L1. G ⊢ L1 ⫃▪[h, g] L2 → ⦃G, L1⦄ ⊢ T ▪[h, g] d.
 #h #g #G #L2 #T #d #H elim H -G -L2 -T -d
-[ /2 width=1/
+[ /2 width=1 by da_sort/
 | #G #L2 #K2 #V #i #d #HLK2 #_ #IHV #L1 #HL12
   elim (lsubd_drop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
   elim (lsubd_inv_pair2 … H) -H * #K1 [ | -IHV -HLK1 ]
-  [ #HK12 #H destruct /3 width=4/
+  [ #HK12 #H destruct /3 width=4 by da_ldef/
   | #W #d0 #_ #_ #_ #H destruct
   ]
 | #G #L2 #K2 #W #i #d #HLK2 #HW #IHW #L1 #HL12
   elim (lsubd_drop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
   elim (lsubd_inv_pair2 … H) -H * #K1 [ -HW | -IHW ]
-  [ #HK12 #H destruct /3 width=4/
+  [ #HK12 #H destruct /3 width=4 by da_ldec/
   | #V #d0 #HV #H0W #_ #_ #H destruct
-    lapply (da_mono … H0W … HW) -H0W -HW #H destruct /3 width=7/
+    lapply (da_mono … H0W … HW) -H0W -HW #H destruct /3 width=7 by da_ldef, da_flat/
   ]
-| /4 width=1/
-| /3 width=1/
+| /4 width=1 by lsubd_pair, da_bind/
+| /3 width=1 by da_flat/
 ]
 qed-.
 
 lemma lsubd_da_conf: ∀h,g,G,L1,T,d. ⦃G, L1⦄ ⊢ T ▪[h, g] d →
                      ∀L2. G ⊢ L1 ⫃▪[h, g] L2 → ⦃G, L2⦄ ⊢ T ▪[h, g] d.
 #h #g #G #L1 #T #d #H elim H -G -L1 -T -d
-[ /2 width=1/
+[ /2 width=1 by da_sort/
 | #G #L1 #K1 #V #i #d #HLK1 #HV #IHV #L2 #HL12
   elim (lsubd_drop_O1_conf … HL12 … HLK1) -L1 #X #H #HLK2
   elim (lsubd_inv_pair1 … H) -H * #K2 [ -HV | -IHV ]
-  [ #HK12 #H destruct /3 width=4/
+  [ #HK12 #H destruct /3 width=4 by da_ldef/
   | #W0 #V0 #d0 #HV0 #HW0 #_ #_ #H1 #H2 destruct
     lapply (da_inv_flat … HV) -HV #H0V0
-    lapply (da_mono … H0V0 … HV0) -H0V0 -HV0 #H destruct /2 width=4/
+    lapply (da_mono … H0V0 … HV0) -H0V0 -HV0 #H destruct /2 width=4 by da_ldec/
   ]
 | #G #L1 #K1 #W #i #d #HLK1 #HW #IHW #L2 #HL12
   elim (lsubd_drop_O1_conf … HL12 … HLK1) -L1 #X #H #HLK2
   elim (lsubd_inv_pair1 … H) -H * #K2 [ -HW | -IHW ]
-  [ #HK12 #H destruct /3 width=4/
+  [ #HK12 #H destruct /3 width=4 by da_ldec/
   | #W0 #V0 #d0 #HV0 #HW0 #_ #H destruct
   ]
-| /4 width=1/
-| /3 width=1/
+| /4 width=1 by lsubd_pair, da_bind/
+| /3 width=1 by da_flat/
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubd_lsubd.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubd_lsubd.ma
index 18670b4f1..270cdbd9d 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubd_lsubd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubd_lsubd.ma
@@ -23,7 +23,7 @@ theorem lsubd_trans: ∀h,g,G. Transitive … (lsubd h g G).
 [ #X #H >(lsubd_inv_atom1 … H) -H //
 | #I #L1 #L #Y #HL1 #IHL1 #X #H
   elim (lsubd_inv_pair1 … H) -H * #L2
-  [ #HL2 #H destruct /3 width=1/
+  [ #HL2 #H destruct /3 width=1 by lsubd_pair/
   | #W #V #d #HV #HW #HL2 #H1 #H2 #H3 destruct
     /3 width=3 by lsubd_beta, lsubd_da_trans/
   ]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqu.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqu.ma
index fa388daca..47bd0eabe 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqu.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqu.ma
@@ -86,5 +86,5 @@ lemma fqu_wf_ind: ∀R:relation3 …. (
                      ∀G1,L1,T1. (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → R G2 L2 T2) →
 		                R G1 L1 T1
 		  ) → ∀G1,L1,T1. R G1 L1 T1.
-#R #HR @(f3_ind … fw) #n #IHn #G1 #L1 #T1 #H destruct /4 width=1 by fqu_fwd_fw/
+#R #HR @(f3_ind … fw) #x #IHx #G1 #L1 #T1 #H destruct /4 width=1 by fqu_fwd_fw/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/gget.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/gget.ma
index eb5c8fdab..1ea9ce7ff 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/gget.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/gget.ma
@@ -74,7 +74,7 @@ lemma gget_total: ∀m,G1. ∃G2. ⬇[m] G1 ≡ G2.
 #m #G1 elim G1 -G1 /3 width=2 by gget_gt, ex_intro/
 #I #V #G1 * #G2 #HG12
 elim (lt_or_eq_or_gt m (|G1|)) #Hm
-[ /3 width=2/
+[ /3 width=2 by gget_lt, ex_intro/
 | destruct /3 width=2 by gget_eq, ex_intro/
 | @ex_intro [2: @gget_gt normalize /2 width=1 by/ | skip ] (**) (* explicit constructor *)
 ]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/gget_gget.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/gget_gget.ma
index c08ab3960..7bd39f09b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/gget_gget.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/gget_gget.ma
@@ -25,7 +25,7 @@ theorem gget_mono: ∀G,G1,m. ⬇[m] G ≡ G1 → ∀G2. ⬇[m] G ≡ G2 → G1
 | #G #Hm #G2 #H
   >(gget_inv_eq … H Hm) -H -Hm //
 | #I #G #G1 #V #Hm #_ #IHG1 #G2 #H
-  lapply (gget_inv_lt … H Hm) -H -Hm /2 width=1/
+  lapply (gget_inv_lt … H Hm) -H -Hm /2 width=1 by/
 ]
 qed-.
 
@@ -33,8 +33,8 @@ lemma gget_dec: ∀G1,G2,m. Decidable (⬇[m] G1 ≡ G2).
 #G1 #G2 #m
 elim (gget_total m G1) #G #HG1
 elim (eq_genv_dec G G2) #HG2
-[ destruct /2 width=1/
+[ destruct /2 width=1 by or_introl/
 | @or_intror #HG12
-  lapply (gget_mono … HG1 … HG12) -HG1 -HG12 /2 width=1/
+  lapply (gget_mono … HG1 … HG12) -HG1 -HG12 /2 width=1 by/
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma
index fdb8b6a72..1d02e6b8b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma
@@ -309,7 +309,7 @@ lemma lift_lref_ge_minus: ∀l,m,i. l + m ≤ i → ⬆[l, m] #(i - m) ≡ #i.
 qed.
 
 lemma lift_lref_ge_minus_eq: ∀l,m,i,j. l + m ≤ i → j = i - m → ⬆[l, m] #j ≡ #i.
-/2 width=1/ qed-.
+/2 width=1 by lift_lref_ge_minus/ qed-.
 
 (* Basic_1: was: lift_r *)
 lemma lift_refl: ∀T,l. ⬆[l, 0] T ≡ T.
@@ -321,7 +321,8 @@ qed.
 
 lemma lift_total: ∀T1,l,m. ∃T2. ⬆[l,m] T1 ≡ T2.
 #T1 elim T1 -T1
-[ * #i /2 width=2/ #l #m elim (lt_or_ge i l) /3 width=2 by lift_lref_lt, lift_lref_ge, ex_intro/
+[ * #i /2 width=2 by lift_sort, lift_gref, ex_intro/
+  #l #m elim (lt_or_ge i l) /3 width=2 by lift_lref_lt, lift_lref_ge, ex_intro/
 | * [ #a ] #I #V1 #T1 #IHV1 #IHT1 #l #m
   elim (IHV1 l m) -IHV1 #V2 #HV12
   [ elim (IHT1 (l+1) m) -IHT1 /3 width=2 by lift_bind, ex_intro/
@@ -335,13 +336,13 @@ lemma lift_split: ∀l1,m2,T1,T2. ⬆[l1, m2] T1 ≡ T2 →
                   ∀l2,m1. l1 ≤ l2 → l2 ≤ l1 + m1 → m1 ≤ m2 →
                   ∃∃T. ⬆[l1, m1] T1 ≡ T & ⬆[l2, m2 - m1] T ≡ T2.
 #l1 #m2 #T1 #T2 #H elim H -l1 -m2 -T1 -T2
-[ /3 width=3/
+[ /3 width=3 by lift_sort, ex2_intro/
 | #i #l1 #m2 #Hil1 #l2 #m1 #Hl12 #_ #_
   lapply (lt_to_le_to_lt … Hil1 Hl12) -Hl12 #Hil2 /4 width=3 by lift_lref_lt, ex2_intro/
 | #i #l1 #m2 #Hil1 #l2 #m1 #_ #Hl21 #Hm12
   lapply (transitive_le … (i+m1) Hl21 ?) /2 width=1 by monotonic_le_plus_l/ -Hl21 #Hl21
   >(plus_minus_m_m m2 m1 ?) /3 width=3 by lift_lref_ge, ex2_intro/
-| /3 width=3/
+| /3 width=3 by lift_gref, ex2_intro/
 | #a #I #V1 #V2 #T1 #T2 #l1 #m2 #_ #_ #IHV #IHT #l2 #m1 #Hl12 #Hl21 #Hm12
   elim (IHV … Hl12 Hl21 Hm12) -IHV #V0 #HV0a #HV0b
   elim (IHT (l2+1) … ? ? Hm12) /3 width=5 by lift_bind, le_S_S, ex2_intro/
@@ -374,7 +375,7 @@ lemma is_lift_dec: ∀T2,l,m. Decidable (∃T1. ⬆[l,m] T1 ≡ T2).
     ]
   | elim (IHV2 l m) -IHV2
     [ * #V1 #HV12 elim (IHT2 l m) -IHT2
-      [ * #T1 #HT12 /4 width=2/
+      [ * #T1 #HT12 /4 width=2 by lift_flat, ex_intro, or_introl/
       | -V1 #HT2 @or_intror * #X #H
         elim (lift_inv_flat2 … H) -H /3 width=2 by ex_intro/
       ]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift_vector.ma
index 44ed6a7b4..577682957 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift_vector.ma
@@ -25,6 +25,6 @@ theorem liftv_mono: ∀Ts,U1s,l,m. ⬆[l,m] Ts ≡ U1s →
 [ #U2s #H >(liftv_inv_nil1 … H) -H //
 | #Ts #U1s #T #U1 #HTU1 #_ #IHTU1s #X #H destruct
   elim (liftv_inv_cons1 … H) -H #U2 #U2s #HTU2 #HTU2s #H destruct
-  >(lift_mono … HTU1 … HTU2) -T /3 width=1/
+  >(lift_mono … HTU1 … HTU2) -T /3 width=1 by eq_f/
 ]
 qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_lpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_lpx_sn.ma
index 70b8931f0..fe4b2b845 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_lpx_sn.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_lpx_sn.ma
@@ -35,11 +35,11 @@ qed-.
 
 theorem lpx_sn_conf: ∀R1,R2. lpx_sn_confluent R1 R2 →
                      confluent2 … (lpx_sn R1) (lpx_sn R2).
-#R1 #R2 #HR12 #L0 @(f_ind … length … L0) -L0 #n #IH *
-[ #_ #X1 #H1 #X2 #H2 -n
+#R1 #R2 #HR12 #L0 @(f_ind … length … L0) -L0 #x #IH *
+[ #_ #X1 #H1 #X2 #H2 -x
   >(lpx_sn_inv_atom1 … H1) -X1
   >(lpx_sn_inv_atom1 … H2) -X2 /2 width=3 by lpx_sn_atom, ex2_intro/
-| #L0 #I #V0 #Hn #X1 #H1 #X2 #H2 destruct
+| #L0 #I #V0 #Hx #X1 #H1 #X2 #H2 destruct
   elim (lpx_sn_inv_pair1 … H1) -H1 #L1 #V1 #HL01 #HV01 #H destruct
   elim (lpx_sn_inv_pair1 … H2) -H2 #L2 #V2 #HL02 #HV02 #H destruct
   elim (IH … HL01 … HL02) -IH normalize // #L #HL1 #HL2