From 2ba2dc23443ad764adab652e06d6f5ed10bd912d Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 18 Jan 2014 22:05:09 +0000
Subject: [PATCH] - commit of the "reduction" component with two additions ...
 - formal bug fix in extended substitution under a binder: now we follow the
 paradigm used for reduction under a binder

---
 .../lambdadelta/basic_2/reduction/cir.ma      | 22 ++---
 .../lambdadelta/basic_2/reduction/cir_lift.ma |  8 +-
 .../lambdadelta/basic_2/reduction/cix.ma      | 26 +++---
 .../lambdadelta/basic_2/reduction/cix_lift.ma | 10 +-
 .../lambdadelta/basic_2/reduction/cnr.ma      | 31 ++++---
 .../lambdadelta/basic_2/reduction/cnr_lift.ma | 18 ++--
 .../lambdadelta/basic_2/reduction/cnx.ma      | 28 +++---
 .../lambdadelta/basic_2/reduction/cnx_lift.ma | 10 +-
 .../lambdadelta/basic_2/reduction/cpr.ma      | 78 ++++++++--------
 .../lambdadelta/basic_2/reduction/cpr_lift.ma | 91 ++++++++++---------
 .../lambdadelta/basic_2/reduction/cpx.ma      | 20 ++--
 .../lambdadelta/basic_2/reduction/cpx_cpys.ma | 28 ++++++
 .../lambdadelta/basic_2/reduction/cpx_lift.ma | 67 +++++++-------
 .../lambdadelta/basic_2/reduction/crr.ma      | 16 ++--
 .../lambdadelta/basic_2/reduction/crr_lift.ma | 72 +++++++--------
 .../lambdadelta/basic_2/reduction/crx.ma      | 23 ++---
 .../lambdadelta/basic_2/reduction/crx_lift.ma | 82 ++++++++---------
 .../basic_2/reduction/lpr_ldrop.ma            |  4 +-
 .../lambdadelta/basic_2/reduction/lpr_lpr.ma  | 20 ++--
 .../lambdadelta/basic_2/reduction/lpx_aaa.ma  | 30 +++---
 .../basic_2/reduction/lpx_ldrop.ma            |  4 +-
 .../lambdadelta/basic_2/relocation/cpy.ma     | 12 +--
 .../lambdadelta/basic_2/relocation/cpy_cpy.ma | 24 +++--
 .../basic_2/relocation/cpy_lift.ma            |  6 +-
 .../lambdadelta/basic_2/substitution/cpys.ma  | 10 +-
 .../basic_2/substitution/cpys_alt.ma          | 11 +--
 .../lambdadelta/basic_2/substitution/lleq.ma  |  7 +-
 .../lambdadelta/basic_2/web/basic_2_src.tbl   |  2 +-
 28 files changed, 394 insertions(+), 366 deletions(-)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cpys.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir.ma
index 276a8a03a..35a28700a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir.ma
@@ -24,35 +24,35 @@ interpretation "context-sensitive irreducibility (term)"
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma cir_inv_delta: ∀G,L,K,V,i. ⇩[0, i] L ≡ K.ⓓV → ⦃G, L⦄ ⊢ 𝐈⦃#i⦄ → ⊥.
-/3 width=3/ qed-.
+lemma cir_inv_delta: ∀G,L,K,V,i. ⇩[i] L ≡ K.ⓓV → ⦃G, L⦄ ⊢ 𝐈⦃#i⦄ → ⊥.
+/3 width=3 by crr_delta/ qed-.
 
 lemma cir_inv_ri2: ∀I,G,L,V,T. ri2 I → ⦃G, L⦄ ⊢ 𝐈⦃②{I}V.T⦄ → ⊥.
-/3 width=1/ qed-.
+/3 width=1 by crr_ri2/ qed-.
 
 lemma cir_inv_ib2: ∀a,I,G,L,V,T. ib2 a I → ⦃G, L⦄ ⊢ 𝐈⦃ⓑ{a,I}V.T⦄ →
                    ⦃G, L⦄ ⊢ 𝐈⦃V⦄ ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ 𝐈⦃T⦄.
-/4 width=1/ qed-.
+/4 width=1 by crr_ib2_sn, crr_ib2_dx, conj/ qed-.
 
 lemma cir_inv_bind: ∀a,I,G,L,V,T. ⦃G, L⦄ ⊢ 𝐈⦃ⓑ{a,I}V.T⦄ →
                     ∧∧ ⦃G, L⦄ ⊢ 𝐈⦃V⦄ & ⦃G, L.ⓑ{I}V⦄ ⊢ 𝐈⦃T⦄ & ib2 a I.
 #a * [ elim a -a ]
-#G #L #V #T #H [ elim H -H /3 width=1/ ]
-elim (cir_inv_ib2 … H) -H /2 width=1/ /3 width=1/
+#G #L #V #T #H [ elim H -H /3 width=1 by crr_ri2, or_introl/ ]
+elim (cir_inv_ib2 … H) -H /3 width=1 by and3_intro, or_introl/
 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/
 generalize in match HVT; -HVT elim T -T //
-* // #a * #U #T #_ #_ #H elim H -H /2 width=1/
+* // #a * #U #T #_ #_ #H elim H -H /2 width=1 by crr_beta, crr_theta/
 qed-.
 
 lemma cir_inv_flat: ∀I,G,L,V,T. ⦃G, L⦄ ⊢ 𝐈⦃ⓕ{I}V.T⦄ →
                     ∧∧ ⦃G, L⦄ ⊢ 𝐈⦃V⦄ & ⦃G, L⦄ ⊢ 𝐈⦃T⦄ & 𝐒⦃T⦄ & I = Appl.
 * #G #L #V #T #H
-[ elim (cir_inv_appl … H) -H /2 width=1/
-| elim (cir_inv_ri2 … H) -H /2 width=1/
+[ elim (cir_inv_appl … H) -H /2 width=1 by and4_intro/
+| elim (cir_inv_ri2 … H) -H //
 ]
 qed-.
 
@@ -70,10 +70,10 @@ lemma tir_atom: ∀G,I. ⦃G, ⋆⦄ ⊢ 𝐈⦃⓪{I}⦄.
 lemma cir_ib2: ∀a,I,G,L,V,T.
                ib2 a I → ⦃G, L⦄ ⊢ 𝐈⦃V⦄ → ⦃G, L.ⓑ{I}V⦄ ⊢ 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ 𝐈⦃ⓑ{a,I}V.T⦄.
 #a #I #G #L #V #T #HI #HV #HT #H
-elim (crr_inv_ib2 … HI H) -HI -H /2 width=1/
+elim (crr_inv_ib2 … HI H) -HI -H /2 width=1 by/
 qed.
 
 lemma cir_appl: ∀G,L,V,T. ⦃G, L⦄ ⊢ 𝐈⦃V⦄ → ⦃G, L⦄ ⊢ 𝐈⦃T⦄ →  𝐒⦃T⦄ → ⦃G, L⦄ ⊢ 𝐈⦃ⓐV.T⦄.
 #G #L #V #T #HV #HT #H1 #H2
-elim (crr_inv_appl … H2) -H2 /2 width=1/
+elim (crr_inv_appl … H2) -H2 /2 width=1 by/
 qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma
index 8ddf8c33b..0c518239a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma
@@ -19,10 +19,10 @@ include "basic_2/reduction/cir.ma".
 
 (* Properties on relocation *************************************************)
 
-lemma cir_lift: ∀G,K,T. ⦃G, K⦄ ⊢ 𝐈⦃T⦄ → ∀L,d,e. ⇩[d, e] L ≡ K →
+lemma cir_lift: ∀G,K,T. ⦃G, K⦄ ⊢ 𝐈⦃T⦄ → ∀L,s,d,e. ⇩[s, d, e] L ≡ K →
                 ∀U. ⇧[d, e] T ≡ U → ⦃G, L⦄ ⊢ 𝐈⦃U⦄.
-/3 width=7 by crr_inv_lift/ qed.
+/3 width=8 by crr_inv_lift/ qed.
 
-lemma cir_inv_lift: ∀G,L,U. ⦃G, L⦄ ⊢ 𝐈⦃U⦄ → ∀K,d,e. ⇩[d, e] L ≡ K →
+lemma cir_inv_lift: ∀G,L,U. ⦃G, L⦄ ⊢ 𝐈⦃U⦄ → ∀K,s,d,e. ⇩[s, d, e] L ≡ K →
                     ∀T. ⇧[d, e] T ≡ U → ⦃G, K⦄ ⊢ 𝐈⦃T⦄.
-/3 width=7/ qed-.
+/3 width=8 by crr_lift/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cix.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cix.ma
index fc1de0d4c..d7da41971 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cix.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cix.ma
@@ -27,44 +27,44 @@ interpretation "context-sensitive extended irreducibility (term)"
 (* Basic inversion lemmas ***************************************************)
 
 lemma cix_inv_sort: ∀h,g,G,L,k,l. deg h g k (l+1) → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃⋆k⦄ → ⊥.
-/3 width=2/ qed-.
+/3 width=2 by crx_sort/ qed-.
 
-lemma cix_inv_delta: ∀h,g,I,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃#i⦄ → ⊥.
-/3 width=4/ qed-.
+lemma cix_inv_delta: ∀h,g,I,G,L,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃#i⦄ → ⊥.
+/3 width=4 by crx_delta/ qed-.
 
 lemma cix_inv_ri2: ∀h,g,I,G,L,V,T. ri2 I → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃②{I}V.T⦄ → ⊥.
-/3 width=1/ qed-.
+/3 width=1 by crx_ri2/ qed-.
 
 lemma cix_inv_ib2: ∀h,g,a,I,G,L,V,T. ib2 a I → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃ⓑ{a,I}V.T⦄ →
                    ⦃G, L⦄ ⊢ 𝐈[h, g]⦃V⦄ ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ 𝐈[h, g]⦃T⦄.
-/4 width=1/ qed-.
+/4 width=1 by crx_ib2_sn, crx_ib2_dx, conj/ qed-.
 
 lemma cix_inv_bind: ∀h,g,a,I,G,L,V,T. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃ⓑ{a,I}V.T⦄ →
                     ∧∧ ⦃G, L⦄ ⊢ 𝐈[h, g]⦃V⦄ & ⦃G, L.ⓑ{I}V⦄ ⊢ 𝐈[h, g]⦃T⦄ & ib2 a I.
 #h #g #a * [ elim a -a ]
-#G #L #V #T #H [ elim H -H /3 width=1/ ]
-elim (cix_inv_ib2 … H) -H /2 width=1/ /3 width=1/
+#G #L #V #T #H [ elim H -H /3 width=1 by crx_ri2, or_introl/ ]
+elim (cix_inv_ib2 … H) -H /3 width=1 by and3_intro, or_introl/
 qed-.
 
 lemma cix_inv_appl: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃ⓐV.T⦄ →
                     ∧∧ ⦃G, L⦄ ⊢ 𝐈[h, g]⦃V⦄ & ⦃G, L⦄ ⊢ 𝐈[h, g]⦃T⦄ & 𝐒⦃T⦄.
 #h #g #G #L #V #T #HVT @and3_intro /3 width=1/
 generalize in match HVT; -HVT elim T -T //
-* // #a * #U #T #_ #_ #H elim H -H /2 width=1/
+* // #a * #U #T #_ #_ #H elim H -H /2 width=1 by crx_beta, crx_theta/
 qed-.
 
 lemma cix_inv_flat: ∀h,g,I,G,L,V,T. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃ⓕ{I}V.T⦄ →
                     ∧∧ ⦃G, L⦄ ⊢ 𝐈[h, g]⦃V⦄ & ⦃G, L⦄ ⊢ 𝐈[h, g]⦃T⦄ & 𝐒⦃T⦄ & I = Appl.
 #h #g * #G #L #V #T #H
-[ elim (cix_inv_appl … H) -H /2 width=1/
-| elim (cix_inv_ri2 … H) -H /2 width=1/
+[ elim (cix_inv_appl … H) -H /2 width=1 by and4_intro/
+| elim (cix_inv_ri2 … H) -H //
 ]
 qed-.
 
 (* Basic forward lemmas *****************************************************)
 
 lemma cix_inv_cir: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ 𝐈⦃T⦄.
-/3 width=1/ qed-.
+/3 width=1 by crr_crx/ qed-.
 
 (* Basic properties *********************************************************)
 
@@ -84,10 +84,10 @@ qed.
 lemma cix_ib2: ∀h,g,a,I,G,L,V,T. ib2 a I → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃V⦄ → ⦃G, L.ⓑ{I}V⦄ ⊢ 𝐈[h, g]⦃T⦄ →
                                ⦃G, L⦄ ⊢ 𝐈[h, g]⦃ⓑ{a,I}V.T⦄.
 #h #g #a #I #G #L #V #T #HI #HV #HT #H
-elim (crx_inv_ib2 … HI H) -HI -H /2 width=1/
+elim (crx_inv_ib2 … HI H) -HI -H /2 width=1 by/
 qed.
 
 lemma cix_appl: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃V⦄ → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃T⦄ →  𝐒⦃T⦄ → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃ⓐV.T⦄.
 #h #g #G #L #V #T #HV #HT #H1 #H2
-elim (crx_inv_appl … H2) -H2 /2 width=1/
+elim (crx_inv_appl … H2) -H2 /2 width=1 by/
 qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cix_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cix_lift.ma
index 95776767a..72d5dbaac 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cix_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cix_lift.ma
@@ -19,17 +19,17 @@ include "basic_2/reduction/cix.ma".
 
 (* Advanced properties ******************************************************)
 
-lemma cix_lref: ∀h,g,G,L,i. ⇩[0, i] L ≡ ⋆ → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃#i⦄.
+lemma cix_lref: ∀h,g,G,L,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃#i⦄.
 #h #g #G #L #i #HL #H elim (crx_inv_lref … H) -h #I #K #V #HLK
 lapply (ldrop_mono … HLK … HL) -L -i #H destruct
 qed.
 
 (* Properties on relocation *************************************************)
 
-lemma cix_lift: ∀h,g,G,K,T. ⦃G, K⦄ ⊢ 𝐈[h, g]⦃T⦄ → ∀L,d,e. ⇩[d, e] L ≡ K →
+lemma cix_lift: ∀h,g,G,K,T. ⦃G, K⦄ ⊢ 𝐈[h, g]⦃T⦄ → ∀L,s,d,e. ⇩[s, d, e] L ≡ K →
                 ∀U. ⇧[d, e] T ≡ U → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃U⦄.
-/3 width=7 by crx_inv_lift/ qed.
+/3 width=8 by crx_inv_lift/ qed.
 
-lemma cix_inv_lift: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃U⦄ → ∀K,d,e. ⇩[d, e] L ≡ K →
+lemma cix_inv_lift: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃U⦄ → ∀K,s,d,e. ⇩[s, d, e] L ≡ K →
                     ∀T. ⇧[d, e] T ≡ U → ⦃G, K⦄ ⊢ 𝐈[h, g]⦃T⦄.
-/3 width=7/ qed-.
+/3 width=8 by crx_lift/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr.ma
index c1a44b729..34d95faae 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr.ma
@@ -25,52 +25,53 @@ interpretation
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma cnr_inv_delta: ∀G,L,K,V,i. ⇩[0, i] L ≡ K.ⓓV → ⦃G, L⦄ ⊢ 𝐍⦃#i⦄ → ⊥.
+lemma cnr_inv_delta: ∀G,L,K,V,i. ⇩[i] L ≡ K.ⓓV → ⦃G, L⦄ ⊢ 𝐍⦃#i⦄ → ⊥.
 #G #L #K #V #i #HLK #H
 elim (lift_total V 0 (i+1)) #W #HVW
-lapply (H W ?) -H [ /3 width=6/ ] -HLK #H destruct
+lapply (H W ?) -H [ /3 width=6 by cpr_delta/ ] -HLK #H destruct
 elim (lift_inv_lref2_be … HVW) -HVW //
 qed-.
 
 lemma cnr_inv_abst: ∀a,G,L,V,T. ⦃G, L⦄ ⊢ 𝐍⦃ⓛ{a}V.T⦄ → ⦃G, L⦄ ⊢ 𝐍⦃V⦄ ∧ ⦃G, L.ⓛV⦄ ⊢ 𝐍⦃T⦄.
 #a #G #L #V1 #T1 #HVT1 @conj
-[ #V2 #HV2 lapply (HVT1 (ⓛ{a}V2.T1) ?) -HVT1 /2 width=2/ -HV2 #H destruct //
-| #T2 #HT2 lapply (HVT1 (ⓛ{a}V1.T2) ?) -HVT1 /2 width=2/ -HT2 #H destruct //
+[ #V2 #HV2 lapply (HVT1 (ⓛ{a}V2.T1) ?) -HVT1 /2 width=2 by cpr_pair_sn/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (ⓛ{a}V1.T2) ?) -HVT1 /2 width=2 by cpr_bind/ -HT2 #H destruct //
 ]
 qed-.
 
 lemma cnr_inv_abbr: ∀G,L,V,T. ⦃G, L⦄ ⊢ 𝐍⦃-ⓓV.T⦄ → ⦃G, L⦄ ⊢ 𝐍⦃V⦄ ∧ ⦃G, L.ⓓV⦄ ⊢ 𝐍⦃T⦄.
 #G #L #V1 #T1 #HVT1 @conj
-[ #V2 #HV2 lapply (HVT1 (-ⓓV2.T1) ?) -HVT1 /2 width=2/ -HV2 #H destruct //
-| #T2 #HT2 lapply (HVT1 (-ⓓV1.T2) ?) -HVT1 /2 width=2/ -HT2 #H destruct //
+[ #V2 #HV2 lapply (HVT1 (-ⓓV2.T1) ?) -HVT1 /2 width=2 by cpr_pair_sn/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (-ⓓV1.T2) ?) -HVT1 /2 width=2 by cpr_bind/ -HT2 #H destruct //
 ]
 qed-.
 
 lemma cnr_inv_zeta: ∀G,L,V,T. ⦃G, L⦄ ⊢ 𝐍⦃+ⓓV.T⦄ → ⊥.
 #G #L #V #T #H elim (is_lift_dec T 0 1)
 [ * #U #HTU
-  lapply (H U ?) -H /2 width=3/ #H destruct
+  lapply (H U ?) -H /2 width=3 by cpr_zeta/ #H destruct
   elim (lift_inv_pair_xy_y … HTU)
 | #HT
-  elim (cpr_delift G (⋆) V T (⋆. ⓓV) 0) // #T2 #T1 #HT2 #HT12
-  lapply (H (+ⓓV.T2) ?) -H /4 width=1/ -HT2 #H destruct /3 width=2/
+  elim (cpr_delift G (⋆) V T (⋆. ⓓV) 0) //
+  #T2 #T1 #HT2 #HT12 lapply (H (+ⓓV.T2) ?) -H /4 width=1 by tpr_cpr, cpr_bind/ -HT2
+  #H destruct /3 width=2 by ex_intro/
 ]
 qed-.
 
 lemma cnr_inv_appl: ∀G,L,V,T. ⦃G, L⦄ ⊢ 𝐍⦃ⓐV.T⦄ → ∧∧ ⦃G, L⦄ ⊢ 𝐍⦃V⦄ & ⦃G, L⦄ ⊢ 𝐍⦃T⦄ & 𝐒⦃T⦄.
 #G #L #V1 #T1 #HVT1 @and3_intro
-[ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct //
-| #T2 #HT2 lapply (HVT1 (ⓐV1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct //
+[ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1 by cpr_pair_sn/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (ⓐV1.T2) ?) -HVT1 /2 width=1 by cpr_flat/ -HT2 #H destruct //
 | generalize in match HVT1; -HVT1 elim T1 -T1 * // #a * #W1 #U1 #_ #_ #H
   [ elim (lift_total V1 0 1) #V2 #HV12
-    lapply (H (ⓓ{a}W1.ⓐV2.U1) ?) -H /3 width=3/ -HV12 #H destruct
-  | lapply (H (ⓓ{a}ⓝW1.V1.U1) ?) -H /3 width=1/ #H destruct
+    lapply (H (ⓓ{a}W1.ⓐV2.U1) ?) -H /3 width=3 by tpr_cpr, cpr_theta/ -HV12 #H destruct
+  | lapply (H (ⓓ{a}ⓝW1.V1.U1) ?) -H /3 width=1 by tpr_cpr, cpr_beta/ #H destruct
 ]
 qed-.
 
 lemma cnr_inv_tau: ∀G,L,V,T. ⦃G, L⦄ ⊢ 𝐍⦃ⓝV.T⦄ → ⊥.
-#G #L #V #T #H lapply (H T ?) -H /2 width=1/ #H
-@discr_tpair_xy_y //
+#G #L #V #T #H lapply (H T ?) -H
+/2 width=4 by cpr_tau, discr_tpair_xy_y/
 qed-.
 
 (* Basic properties *********************************************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma
index ed4280a6a..9f29fe9a8 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma
@@ -20,7 +20,7 @@ include "basic_2/reduction/cnr.ma".
 (* Advanced properties ******************************************************)
 
 (* Basic_1: was only: nf2_csort_lref *)
-lemma cnr_lref_atom: ∀G,L,i. ⇩[0, i] L ≡ ⋆ → ⦃G, L⦄ ⊢ 𝐍⦃#i⦄.
+lemma cnr_lref_atom: ∀G,L,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ 𝐍⦃#i⦄.
 #G #L #i #HL #X #H
 elim (cpr_inv_lref1 … H) -H // *
 #K #V1 #V2 #HLK #_ #_
@@ -28,7 +28,7 @@ lapply (ldrop_mono … HL … HLK) -L #H destruct
 qed.
 
 (* Basic_1: was: nf2_lref_abst *)
-lemma cnr_lref_abst: ∀G,L,K,V,i. ⇩[0, i] L ≡ K. ⓛV → ⦃G, L⦄ ⊢ 𝐍⦃#i⦄.
+lemma cnr_lref_abst: ∀G,L,K,V,i. ⇩[i] L ≡ K. ⓛV → ⦃G, L⦄ ⊢ 𝐍⦃#i⦄.
 #G #L #K #V #i #HLK #X #H
 elim (cpr_inv_lref1 … H) -H // *
 #K0 #V1 #V2 #HLK0 #_ #_
@@ -38,20 +38,20 @@ qed.
 (* Relocation properties ****************************************************)
 
 (* Basic_1: was: nf2_lift *)
-lemma cnr_lift: ∀G,L0,L,T,T0,d,e. ⦃G, L⦄ ⊢ 𝐍⦃T⦄ →
-                ⇩[d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → ⦃G, L0⦄ ⊢ 𝐍⦃T0⦄.
-#G #L0 #L #T #T0 #d #e #HLT #HL0 #HT0 #X #H
+lemma cnr_lift: ∀G,L0,L,T,T0,s,d,e. ⦃G, L⦄ ⊢ 𝐍⦃T⦄ →
+                ⇩[s, d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → ⦃G, L0⦄ ⊢ 𝐍⦃T0⦄.
+#G #L0 #L #T #T0 #s #d #e #HLT #HL0 #HT0 #X #H
 elim (cpr_inv_lift1 … H … HL0 … HT0) -L0 #T1 #HT10 #HT1
 <(HLT … HT1) in HT0; -L #HT0
 >(lift_mono … HT10 … HT0) -T1 -X //
 qed.
 
 (* Note: this was missing in basic_1 *)
-lemma cnr_inv_lift: ∀G,L0,L,T,T0,d,e. ⦃G, L0⦄ ⊢ 𝐍⦃T0⦄ →
-                    ⇩[d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → ⦃G, L⦄ ⊢ 𝐍⦃T⦄.
-#G #L0 #L #T #T0 #d #e #HLT0 #HL0 #HT0 #X #H
+lemma cnr_inv_lift: ∀G,L0,L,T,T0,s,d,e. ⦃G, L0⦄ ⊢ 𝐍⦃T0⦄ →
+                    ⇩[s, d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → ⦃G, L⦄ ⊢ 𝐍⦃T⦄.
+#G #L0 #L #T #T0 #s #d #e #HLT0 #HL0 #HT0 #X #H
 elim (lift_total X d e) #X0 #HX0
 lapply (cpr_lift … H … HL0 … HT0 … HX0) -L #HTX0
 >(HLT0 … HTX0) in HX0; -L0 -X0 #H
->(lift_inj … H … HT0) -T0 -X -d -e //
+>(lift_inj … H … HT0) -T0 -X -s -d -e //
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma
index ba3c976ac..9954e6edb 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma
@@ -30,41 +30,42 @@ interpretation
 lemma cnx_inv_sort: ∀h,g,G,L,k. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃⋆k⦄ → deg h g k 0.
 #h #g #G #L #k #H elim (deg_total h g k)
 #l @(nat_ind_plus … l) -l // #l #_ #Hkl
-lapply (H (⋆(next h k)) ?) -H /2 width=2/ -L -l #H destruct -H -e0 (**) (* destruct does not remove some premises *)
+lapply (H (⋆(next h k)) ?) -H /2 width=2 by cpx_sort/ -L -l #H destruct -H -e0 (**) (* destruct does not remove some premises *)
 lapply (next_lt h k) >e1 -e1 #H elim (lt_refl_false … H)
 qed-.
 
-lemma cnx_inv_delta: ∀h,g,I,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃#i⦄ → ⊥.
+lemma cnx_inv_delta: ∀h,g,I,G,L,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃#i⦄ → ⊥.
 #h #g #I #G #L #K #V #i #HLK #H
 elim (lift_total V 0 (i+1)) #W #HVW
-lapply (H W ?) -H [ /3 width=7/ ] -HLK #H destruct
+lapply (H W ?) -H [ /3 width=7 by cpx_delta/ ] -HLK #H destruct
 elim (lift_inv_lref2_be … HVW) -HVW //
 qed-.
 
 lemma cnx_inv_abst: ∀h,g,a,G,L,V,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃ⓛ{a}V.T⦄ →
                     ⦃G, L⦄ ⊢ 𝐍[h, g]⦃V⦄ ∧ ⦃G, L.ⓛV⦄ ⊢ 𝐍[h, g]⦃T⦄.
 #h #g #a #G #L #V1 #T1 #HVT1 @conj
-[ #V2 #HV2 lapply (HVT1 (ⓛ{a}V2.T1) ?) -HVT1 /2 width=2/ -HV2 #H destruct //
-| #T2 #HT2 lapply (HVT1 (ⓛ{a}V1.T2) ?) -HVT1 /2 width=2/ -HT2 #H destruct //
+[ #V2 #HV2 lapply (HVT1 (ⓛ{a}V2.T1) ?) -HVT1 /2 width=2 by cpx_pair_sn/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (ⓛ{a}V1.T2) ?) -HVT1 /2 width=2 by cpx_bind/ -HT2 #H destruct //
 ]
 qed-.
 
 lemma cnx_inv_abbr: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃-ⓓV.T⦄ →
                     ⦃G, L⦄ ⊢ 𝐍[h, g]⦃V⦄ ∧ ⦃G, L.ⓓV⦄ ⊢ 𝐍[h, g]⦃T⦄.
 #h #g #G #L #V1 #T1 #HVT1 @conj
-[ #V2 #HV2 lapply (HVT1 (-ⓓV2.T1) ?) -HVT1 /2 width=2/ -HV2 #H destruct //
-| #T2 #HT2 lapply (HVT1 (-ⓓV1.T2) ?) -HVT1 /2 width=2/ -HT2 #H destruct //
+[ #V2 #HV2 lapply (HVT1 (-ⓓV2.T1) ?) -HVT1 /2 width=2 by cpx_pair_sn/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (-ⓓV1.T2) ?) -HVT1 /2 width=2 by cpx_bind/ -HT2 #H destruct //
 ]
 qed-.
 
 lemma cnx_inv_zeta: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃+ⓓV.T⦄ → ⊥.
 #h #g #G #L #V #T #H elim (is_lift_dec T 0 1)
 [ * #U #HTU
-  lapply (H U ?) -H /2 width=3/ #H destruct
+  lapply (H U ?) -H /2 width=3 by cpx_zeta/ #H destruct
   elim (lift_inv_pair_xy_y … HTU)
 | #HT
   elim (cpr_delift G(⋆) V T (⋆.ⓓV) 0) // #T2 #T1 #HT2 #HT12
-  lapply (H (+ⓓV.T2) ?) -H /5 width=1/ -HT2 #H destruct /3 width=2/
+  lapply (H (+ⓓV.T2) ?) -H /5 width=1 by cpr_cpx, tpr_cpr, cpr_bind/ -HT2
+  #H destruct /3 width=2 by ex_intro/
 ]
 qed-.
 
@@ -77,19 +78,20 @@ lemma cnx_inv_appl: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃ⓐV.T⦄ →
   [ elim (lift_total V1 0 1) #V2 #HV12
     lapply (H (ⓓ{a}W1.ⓐV2.U1) ?) -H /3 width=3/ -HV12 #H destruct
   | lapply (H (ⓓ{a}ⓝW1.V1.U1) ?) -H /3 width=1/ #H destruct
+  ]
 ]
 qed-.
 
 lemma cnx_inv_tau: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃ⓝV.T⦄ → ⊥.
-#h #g #G #L #V #T #H lapply (H T ?) -H /2 width=1/ #H
-@discr_tpair_xy_y //
+#h #g #G #L #V #T #H lapply (H T ?) -H
+/2 width=4 by cpx_tau, discr_tpair_xy_y/
 qed-.
 
 (* Basic forward lemmas *****************************************************)
 
 lemma cnx_fwd_cnr: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍⦃T⦄.
 #h #g #G #L #T #H #U #HTU
-@H /2 width=1/ (**) (* auto fails because a δ-expansion gets in the way *)
+@H /2 width=1 by cpr_cpx/ (**) (* auto fails because a δ-expansion gets in the way *)
 qed-.
 
 (* Basic properties *********************************************************)
@@ -101,7 +103,7 @@ qed.
 
 lemma cnx_sort_iter: ∀h,g,G,L,k,l. deg h g k l → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃⋆((next h)^l k)⦄.
 #h #g #G #L #k #l #Hkl
-lapply (deg_iter … l Hkl) -Hkl <minus_n_n /2 width=1/
+lapply (deg_iter … l Hkl) -Hkl <minus_n_n /2 width=1 by cnx_sort/
 qed.
 
 lemma cnx_abst: ∀h,g,a,G,L,W,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃W⦄ → ⦃G, L.ⓛW⦄ ⊢ 𝐍[h, g]⦃T⦄ →
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_lift.ma
index 8e0c4ef0e..f52149d5b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_lift.ma
@@ -19,7 +19,7 @@ include "basic_2/reduction/cnx.ma".
 
 (* Advanced properties ******************************************************)
 
-lemma cnx_lref_atom: ∀h,g,G,L,i. ⇩[0, i] L ≡ ⋆ → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃#i⦄.
+lemma cnx_lref_atom: ∀h,g,G,L,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃#i⦄.
 #h #g #G #L #i #HL #X #H
 elim (cpx_inv_lref1 … H) -H // *
 #I #K #V1 #V2 #HLK #_ #_
@@ -28,17 +28,17 @@ qed.
 
 (* Relocation properties ****************************************************)
 
-lemma cnx_lift: ∀h,g,G,L0,L,T,T0,d,e. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → ⇩[d, e] L0 ≡ L →
+lemma cnx_lift: ∀h,g,G,L0,L,T,T0,s,d,e. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → ⇩[s, d, e] L0 ≡ L →
                 ⇧[d, e] T ≡ T0 → ⦃G, L0⦄ ⊢ 𝐍[h, g]⦃T0⦄.
-#h #g #G #L0 #L #T #T0 #d #e #HLT #HL0 #HT0 #X #H
+#h #g #G #L0 #L #T #T0 #s #d #e #HLT #HL0 #HT0 #X #H
 elim (cpx_inv_lift1 … H … HL0 … HT0) -L0 #T1 #HT10 #HT1
 <(HLT … HT1) in HT0; -L #HT0
 >(lift_mono … HT10 … HT0) -T1 -X //
 qed.
 
-lemma cnx_inv_lift: ∀h,g,G,L0,L,T,T0,d,e. ⦃G, L0⦄ ⊢ 𝐍[h, g]⦃T0⦄ → ⇩[d, e] L0 ≡ L →
+lemma cnx_inv_lift: ∀h,g,G,L0,L,T,T0,s,d,e. ⦃G, L0⦄ ⊢ 𝐍[h, g]⦃T0⦄ → ⇩[s, d, e] L0 ≡ L →
                     ⇧[d, e] T ≡ T0 → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄.
-#h #g #G #L0 #L #T #T0 #d #e #HLT0 #HL0 #HT0 #X #H
+#h #g #G #L0 #L #T #T0 #s #d #e #HLT0 #HL0 #HT0 #X #H
 elim (lift_total X d e) #X0 #HX0
 lapply (cpx_lift … H … HL0 … HT0 … HX0) -L #HTX0
 >(HLT0 … HTX0) in HX0; -L0 -X0 #H
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma
index 3c0514a3c..7fcfa3f32 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma
@@ -26,7 +26,7 @@ include "basic_2/relocation/lsubr.ma".
 inductive cpr: relation4 genv lenv term term ≝
 | cpr_atom : ∀I,G,L. cpr G L (⓪{I}) (⓪{I})
 | cpr_delta: ∀G,L,K,V,V2,W2,i.
-             ⇩[0, i] L ≡ K. ⓓV → cpr G K V V2 →
+             ⇩[i] L ≡ K. ⓓV → cpr G K V V2 →
              ⇧[0, i + 1] V2 ≡ W2 → cpr G L (#i) W2
 | cpr_bind : ∀a,I,G,L,V1,V2,T1,T2.
              cpr G L V1 V2 → cpr G (L.ⓑ{I}V1) T1 T2 →
@@ -54,10 +54,11 @@ lemma lsubr_cpr_trans: ∀G. lsub_trans … (cpr G) lsubr.
 #G #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2
 [ //
 | #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
-  elim (lsubr_fwd_ldrop2_abbr … HL12 … HLK1) -L1 * /3 width=6/
-|3,7: /4 width=1/
-|4,6: /3 width=1/
-|5,8: /4 width=3/
+  elim (lsubr_fwd_ldrop2_abbr … HL12 … HLK1) -L1 *
+  /3 width=6 by cpr_delta/
+|3,7: /4 width=1 by lsubr_bind, cpr_bind, cpr_beta/
+|4,6: /3 width=1 by cpr_flat, cpr_tau/
+|5,8: /4 width=3 by lsubr_bind, cpr_zeta, cpr_theta/
 ]
 qed-.
 
@@ -69,47 +70,49 @@ qed.
 
 (* Basic_1: includes by definition: pr0_refl *)
 lemma cpr_refl: ∀G,T,L. ⦃G, L⦄ ⊢ T ➡ T.
-#G #T elim T -T // * /2 width=1/
+#G #T elim T -T // * /2 width=1 by cpr_bind, cpr_flat/
 qed.
 
 (* Basic_1: was: pr2_head_1 *)
 lemma cpr_pair_sn: ∀I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡ V2 →
                    ∀T. ⦃G, L⦄ ⊢ ②{I}V1.T ➡ ②{I}V2.T.
-* /2 width=1/ qed.
+* /2 width=1 by cpr_bind, cpr_flat/ qed.
 
-lemma cpr_delift: ∀G,K,V,T1,L,d. ⇩[0, d] L ≡ (K.ⓓV) →
+lemma cpr_delift: ∀G,K,V,T1,L,d. ⇩[d] L ≡ (K.ⓓV) →
                   ∃∃T2,T. ⦃G, L⦄ ⊢ T1 ➡ T2 & ⇧[d, 1] T ≡ T2.
 #G #K #V #T1 elim T1 -T1
-[ * #i #L #d #HLK /2 width=4/
-  elim (lt_or_eq_or_gt i d) #Hid [1,3: /3 width=4/ ]
+[ * /2 width=4 by cpr_atom, lift_sort, lift_gref, ex2_2_intro/
+  #i #L #d #HLK elim (lt_or_eq_or_gt i d)
+  #Hid [1,3: /3 width=4 by cpr_atom, lift_lref_ge_minus, lift_lref_lt, ex2_2_intro/ ]
   destruct
   elim (lift_total V 0 (i+1)) #W #HVW
-  elim (lift_split … HVW i i) // /3 width=6/
+  elim (lift_split … HVW i i) /3 width=6 by cpr_delta, ex2_2_intro/
 | * [ #a ] #I #W1 #U1 #IHW1 #IHU1 #L #d #HLK
   elim (IHW1 … HLK) -IHW1 #W2 #W #HW12 #HW2
-  [ elim (IHU1 (L. ⓑ{I}W1) (d+1)) -IHU1 /2 width=1/ -HLK /3 width=9/
-  | elim (IHU1 … HLK) -IHU1 -HLK /3 width=8/
+  [ elim (IHU1 (L. ⓑ{I}W1) (d+1)) -IHU1 /3 width=9 by ldrop_drop, cpr_bind, lift_bind, ex2_2_intro/
+  | elim (IHU1 … HLK) -IHU1 -HLK /3 width=8 by cpr_flat, lift_flat, ex2_2_intro/
   ]
 ]
 qed-.
 
 lemma cpr_append: ∀G. l_appendable_sn … (cpr G).
-#G #K #T1 #T2 #H elim H -G -K -T1 -T2 // /2 width=1/ /2 width=3/
+#G #K #T1 #T2 #H elim H -G -K -T1 -T2
+/2 width=3 by cpr_bind, cpr_flat, cpr_zeta, cpr_tau, cpr_beta, cpr_theta/
 #G #K #K0 #V1 #V2 #W2 #i #HK0 #_ #HVW2 #IHV12 #L
 lapply (ldrop_fwd_length_lt2 … HK0) #H
 @(cpr_delta … (L@@K0) V1 … HVW2) //
-@(ldrop_O1_append_sn_le … HK0) /2 width=2/ (**) (* /3/ does not work *)
+@(ldrop_O1_append_sn_le … HK0) /2 width=2 by lt_to_le/ (**) (* /3/ does not work *)
 qed.
 
 (* Basic inversion lemmas ***************************************************)
 
 fact cpr_inv_atom1_aux: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ∀I. T1 = ⓪{I} →
                         T2 = ⓪{I} ∨
-                        ∃∃K,V,V2,i. ⇩[O, i] L ≡ K. ⓓV & ⦃G, K⦄ ⊢ V ➡ V2 &
+                        ∃∃K,V,V2,i. ⇩[i] L ≡ K. ⓓV & ⦃G, K⦄ ⊢ V ➡ V2 &
                                     ⇧[O, i + 1] V2 ≡ T2 & I = LRef i.
 #G #L #T1 #T2 * -G -L -T1 -T2
-[ #I #G #L #J #H destruct /2 width=1/
-| #L #G #K #V #V2 #T2 #i #HLK #HV2 #HVT2 #J #H destruct /3 width=8/
+[ #I #G #L #J #H destruct /2 width=1 by or_introl/
+| #L #G #K #V #V2 #T2 #i #HLK #HV2 #HVT2 #J #H destruct /3 width=8 by ex4_4_intro, or_intror/
 | #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
 | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
 | #G #L #V #T1 #T #T2 #_ #_ #J #H destruct
@@ -121,7 +124,7 @@ qed-.
 
 lemma cpr_inv_atom1: ∀I,G,L,T2. ⦃G, L⦄ ⊢ ⓪{I} ➡ T2 →
                      T2 = ⓪{I} ∨
-                     ∃∃K,V,V2,i. ⇩[O, i] L ≡ K. ⓓV & ⦃G, K⦄ ⊢ V ➡ V2 &
+                     ∃∃K,V,V2,i. ⇩[i] L ≡ K. ⓓV & ⦃G, K⦄ ⊢ V ➡ V2 &
                                  ⇧[O, i + 1] V2 ≡ T2 & I = LRef i.
 /2 width=3 by cpr_inv_atom1_aux/ qed-.
 
@@ -135,11 +138,11 @@ qed-.
 (* Basic_1: includes: pr0_gen_lref pr2_gen_lref *)
 lemma cpr_inv_lref1: ∀G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡ T2 →
                      T2 = #i ∨
-                     ∃∃K,V,V2. ⇩[O, i] L ≡ K. ⓓV & ⦃G, K⦄ ⊢ V ➡ V2 &
+                     ∃∃K,V,V2. ⇩[i] L ≡ K. ⓓV & ⦃G, K⦄ ⊢ V ➡ V2 &
                                ⇧[O, i + 1] V2 ≡ T2.
 #G #L #T2 #i #H
-elim (cpr_inv_atom1 … H) -H /2 width=1/
-* #K #V #V2 #j #HLK #HV2 #HVT2 #H destruct /3 width=6/
+elim (cpr_inv_atom1 … H) -H /2 width=1 by or_introl/
+* #K #V #V2 #j #HLK #HV2 #HVT2 #H destruct /3 width=6 by ex3_3_intro, or_intror/
 qed-.
 
 lemma cpr_inv_gref1: ∀G,L,T2,p. ⦃G, L⦄ ⊢ §p ➡ T2 → T2 = §p.
@@ -158,9 +161,9 @@ fact cpr_inv_bind1_aux: ∀G,L,U1,U2. ⦃G, L⦄ ⊢ U1 ➡ U2 →
 #G #L #U1 #U2 * -L -U1 -U2
 [ #I #G #L #b #J #W1 #U1 #H destruct
 | #L #G #K #V #V2 #W2 #i #_ #_ #_ #b #J #W #U1 #H destruct
-| #a #I #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #b #J #W #U1 #H destruct /3 width=5/
+| #a #I #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #b #J #W #U1 #H destruct /3 width=5 by ex3_2_intro, or_introl/
 | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #b #J #W #U1 #H destruct
-| #G #L #V #T1 #T #T2 #HT1 #HT2 #b #J #W #U1 #H destruct /3 width=3/
+| #G #L #V #T1 #T #T2 #HT1 #HT2 #b #J #W #U1 #H destruct /3 width=3 by ex4_intro, or_intror/
 | #G #L #V #T1 #T2 #_ #b #J #W #U1 #H destruct
 | #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #b #J #W #U1 #H destruct
 | #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #b #J #W #U1 #H destruct
@@ -182,7 +185,8 @@ lemma cpr_inv_abbr1: ∀a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{a}V1.T1 ➡ U2 → (
                      ) ∨
                      ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡ T & ⇧[0, 1] U2 ≡ T & a = true.
 #a #G #L #V1 #T1 #U2 #H
-elim (cpr_inv_bind1 … H) -H * /3 width=3/ /3 width=5/
+elim (cpr_inv_bind1 … H) -H *
+/3 width=5 by ex3_2_intro, ex3_intro, or_introl, or_intror/
 qed-.
 
 (* Basic_1: includes: pr0_gen_abst pr2_gen_abst *)
@@ -191,7 +195,7 @@ lemma cpr_inv_abst1: ∀a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{a}V1.T1 ➡ U2 →
                               U2 = ⓛ{a}V2.T2.
 #a #G #L #V1 #T1 #U2 #H
 elim (cpr_inv_bind1 … H) -H *
-[ /3 width=5/
+[ /3 width=5 by ex3_2_intro/
 | #T #_ #_ #_ #H destruct
 ]
 qed-.
@@ -212,11 +216,11 @@ fact cpr_inv_flat1_aux: ∀G,L,U,U2. ⦃G, L⦄ ⊢ U ➡ U2 →
 [ #I #G #L #J #W1 #U1 #H destruct
 | #G #L #K #V #V2 #W2 #i #_ #_ #_ #J #W #U1 #H destruct
 | #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #J #W #U1 #H destruct
-| #I #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #J #W #U1 #H destruct /3 width=5/
+| #I #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #J #W #U1 #H destruct /3 width=5 by or4_intro0, ex3_2_intro/
 | #G #L #V #T1 #T #T2 #_ #_ #J #W #U1 #H destruct
-| #G #L #V #T1 #T2 #HT12 #J #W #U1 #H destruct /3 width=1/
-| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #J #W #U1 #H destruct /3 width=11/
-| #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HW12 #HT12 #J #W #U1 #H destruct /3 width=13/
+| #G #L #V #T1 #T2 #HT12 #J #W #U1 #H destruct /3 width=1 by or4_intro1, conj/
+| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #J #W #U1 #H destruct /3 width=11 by or4_intro2, ex6_6_intro/
+| #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HW12 #HT12 #J #W #U1 #H destruct /3 width=13 by or4_intro3, ex7_7_intro/
 ]
 qed-.
 
@@ -244,10 +248,10 @@ lemma cpr_inv_appl1: ∀G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓐV1.U1 ➡ U2 →
                                               ⦃G, L⦄ ⊢ W1 ➡ W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ➡ T2 &
                                               U1 = ⓓ{a}W1.T1 & U2 = ⓓ{a}W2.ⓐV2.T2.
 #G #L #V1 #U1 #U2 #H elim (cpr_inv_flat1 … H) -H *
-[ /3 width=5/
+[ /3 width=5 by or3_intro0, ex3_2_intro/
 | #_ #H destruct
-| /3 width=11/
-| /3 width=13/
+| /3 width=11 by or3_intro1, ex5_6_intro/
+| /3 width=13 by or3_intro2, ex6_7_intro/
 ]
 qed-.
 
@@ -271,8 +275,8 @@ lemma cpr_inv_cast1: ∀G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓝ V1. U1 ➡ U2 → (
                               U2 = ⓝ V2. T2
                      ) ∨ ⦃G, L⦄ ⊢ U1 ➡ U2.
 #G #L #V1 #U1 #U2 #H elim (cpr_inv_flat1 … H) -H *
-[ /3 width=5/
-| /2 width=1/
+[ /3 width=5 by ex3_2_intro, or_introl/
+| /2 width=1 by or_intror/
 | #a #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #H destruct
 | #a #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #H destruct
 ]
@@ -285,7 +289,7 @@ lemma cpr_fwd_bind1_minus: ∀I,G,L,V1,T1,T. ⦃G, L⦄ ⊢ -ⓑ{I}V1.T1 ➡ T 
                                     T = -ⓑ{I}V2.T2.
 #I #G #L #V1 #T1 #T #H #b
 elim (cpr_inv_bind1 … H) -H *
-[ #V2 #T2 #HV12 #HT12 #H destruct /3 width=4/
+[ #V2 #T2 #HV12 #HT12 #H destruct /3 width=4 by cpr_bind, ex2_2_intro/
 | #T2 #_ #_ #H destruct
 ]
 qed-.
@@ -301,7 +305,7 @@ lemma cpr_fwd_shift1: ∀G,L1,L,T1,T. ⦃G, L⦄ ⊢ L1 @@ T1 ➡ T →
   [ #V0 #T0 #_ #HT10 #H destruct
     elim (IH … HT10) -IH -HT10 #L2 #T2 #HL12 #H destruct
     >append_length >HL12 -HL12
-    @(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] // /2 width=3/ (**) (* explicit constructor *)
+    @(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] /2 width=3 by trans_eq/ (**) (* explicit constructor *)
   | #T #_ #_ #H destruct
   ]
 ]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_lift.ma
index b384ad2df..dcd6307a7 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_lift.ma
@@ -22,88 +22,89 @@ include "basic_2/reduction/cpr.ma".
 (* Basic_1: includes: pr0_lift pr2_lift *)
 lemma cpr_lift: ∀G. l_liftable (cpr G).
 #G #K #T1 #T2 #H elim H -G -K -T1 -T2
-[ #I #G #K #L #d #e #_ #U1 #H1 #U2 #H2
+[ #I #G #K #L #s #d #e #_ #U1 #H1 #U2 #H2
   >(lift_mono … H1 … H2) -H1 -H2 //
-| #G #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #d #e #HLK #U1 #H #U2 #HWU2
+| #G #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #s #d #e #HLK #U1 #H #U2 #HWU2
   elim (lift_inv_lref1 … H) * #Hid #H destruct
   [ elim (lift_trans_ge … HVW2 … HWU2) -W2 // <minus_plus #W2 #HVW2 #HWU2
-    elim (ldrop_trans_le … HLK … HKV) -K /2 width=2/ #X #HLK #H
-    elim (ldrop_inv_skip2 … H) -H /2 width=1/ -Hid #K #Y #HKV #HVY #H destruct /3 width=8/
-  | lapply (lift_trans_be … HVW2 … HWU2 ? ?) -W2 // /2 width=1/ >plus_plus_comm_23 #HVU2
-    lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K // -Hid /3 width=6/
+    elim (ldrop_trans_le … HLK … HKV) -K /2 width=2 by lt_to_le/ #X #HLK #H
+    elim (ldrop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hid
+    #K #Y #HKV #HVY #H destruct /3 width=9 by cpr_delta/
+  | lapply (lift_trans_be … HVW2 … HWU2 ? ?) -W2 /2 width=1 by le_S/ >plus_plus_comm_23 #HVU2
+    lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K // -Hid /3 width=6 by cpr_delta, ldrop_inv_gen/
   ]
-| #a #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2
+| #a #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #s #d #e #HLK #U1 #H1 #U2 #H2
   elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct
-  elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /4 width=5/
-| #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2
+  elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /4 width=6 by cpr_bind, ldrop_skip/
+| #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #s #d #e #HLK #U1 #H1 #U2 #H2
   elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct
-  elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /3 width=6/
-| #G #K #V #T1 #T #T2 #_ #HT2 #IHT1 #L #d #e #HLK #U1 #H #U2 #HTU2
+  elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /3 width=6 by cpr_flat/
+| #G #K #V #T1 #T #T2 #_ #HT2 #IHT1 #L #s #d #e #HLK #U1 #H #U2 #HTU2
   elim (lift_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct
-  elim (lift_conf_O1 … HTU2 … HT2) -T2 /4 width=5/
-| #G #K #V #T1 #T2 #_ #IHT12 #L #d #e #HLK #U1 #H #U2 #HTU2
-  elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=5/
-| #a #G #K #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L #d #e #HLK #X1 #HX1 #X2 #HX2
+  elim (lift_conf_O1 … HTU2 … HT2) -T2 /4 width=6 by cpr_zeta, ldrop_skip/
+| #G #K #V #T1 #T2 #_ #IHT12 #L #s #d #e #HLK #U1 #H #U2 #HTU2
+  elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=6 by cpr_tau/
+| #a #G #K #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L #s #d #e #HLK #X1 #HX1 #X2 #HX2
   elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct
   elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct
   elim (lift_inv_bind1 … HX2) -HX2 #X #T3 #HX #HT23 #HX2 destruct
-  elim (lift_inv_flat1 … HX) -HX #W3 #V3 #HW23 #HV23 #HX destruct /4 width=5/
-| #a #G #K #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L #d #e #HLK #X1 #HX1 #X2 #HX2
+  elim (lift_inv_flat1 … HX) -HX #W3 #V3 #HW23 #HV23 #HX destruct /4 width=6 by cpr_beta, ldrop_skip/
+| #a #G #K #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L #s #d #e #HLK #X1 #HX1 #X2 #HX2
   elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct
   elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct
   elim (lift_inv_bind1 … HX2) -HX2 #W3 #X #HW23 #HX #HX2 destruct
   elim (lift_inv_flat1 … HX) -HX #V3 #T3 #HV3 #HT23 #HX destruct
-  elim (lift_trans_ge … HV2 … HV3) -V2 // /4 width=5/
+  elim (lift_trans_ge … HV2 … HV3) -V2 /4 width=6 by cpr_theta, ldrop_skip/
 ]
 qed.
 
 (* Basic_1: includes: pr0_gen_lift pr2_gen_lift *)
 lemma cpr_inv_lift1: ∀G. l_deliftable_sn (cpr G).
 #G #L #U1 #U2 #H elim H -G -L -U1 -U2
-[ * #G #L #i #K #d #e #_ #T1 #H
-  [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3/
-  | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3/
-  | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3/
+[ * #G #L #i #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/
   ]
-| #G #L #LV #V #V2 #W2 #i #HLV #HV2 #HVW2 #IHV2 #K #d #e #HLK #T1 #H
+| #G #L #LV #V #V2 #W2 #i #HLV #HV2 #HVW2 #IHV2 #K #s #d #e #HLK #T1 #H
   elim (lift_inv_lref2 … H) -H * #Hid #H destruct
   [ elim (ldrop_conf_lt … HLK … HLV) -L // #L #U #HKL #HLV #HUV
     elim (IHV2 … HLV … HUV) -V #U2 #HUV2 #HU2
-    elim (lift_trans_le … HUV2 … HVW2) -V2 // >minus_plus <plus_minus_m_m // -Hid /3 width=8/
+    elim (lift_trans_le … HUV2 … HVW2) -V2 // >minus_plus <plus_minus_m_m /3 width=8 by cpr_delta, ex2_intro/
   | elim (le_inv_plus_l … Hid) #Hdie #Hei
     lapply (ldrop_conf_ge … HLK … HLV ?) -L // #HKLV
-    elim (lift_split … HVW2 d (i - e + 1)) -HVW2 [4: // |3: /2 width=1/ |2: /3 width=1/ ] -Hid -Hdie
-    #V1 #HV1 >plus_minus // <minus_minus // /2 width=1/ <minus_n_n <plus_n_O /3 width=8/
+    elim (lift_split … HVW2 d (i - e + 1)) -HVW2 [2,3,4: /2 width=1 by le_S_S, le_S/ ] -Hid -Hdie
+    #V1 #HV1 >plus_minus // <minus_minus /2 width=1 by le_S/ <minus_n_n <plus_n_O
+    /3 width=8 by cpr_delta, ex2_intro/
   ]
-| #a #I #G #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H
+| #a #I #G #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #s #d #e #HLK #X #H
   elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
   elim (IHV12 … HLK … HWV1) -IHV12 #W2 #HW12 #HWV2
-  elim (IHU12 … HTU1) -IHU12 -HTU1 /3 width=5/
-| #I #G #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H
+  elim (IHU12 … HTU1) -IHU12 -HTU1 /3 width=6 by cpr_bind, ldrop_skip, lift_bind, ex2_intro/
+| #I #G #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #s #d #e #HLK #X #H
   elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
   elim (IHV12 … HLK … HWV1) -V1
-  elim (IHU12 … HLK … HTU1) -U1 -HLK /3 width=5/
-| #G #L #V #U1 #U #U2 #_ #HU2 #IHU1 #K #d #e #HLK #X #H
+  elim (IHU12 … HLK … HTU1) -U1 -HLK /3 width=6 by cpr_flat, lift_flat, ex2_intro/
+| #G #L #V #U1 #U #U2 #_ #HU2 #IHU1 #K #s #d #e #HLK #X #H
   elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
-  elim (IHU1 (K.ⓓW1) … HTU1) /2 width=1/ -L -U1 #T #HTU #HT1
-  elim (lift_div_le … HU2 … HTU) -U // /3 width=5/
-| #G #L #V #U1 #U2 #_ #IHU12 #K #d #e #HLK #X #H
+  elim (IHU1 (K.ⓓW1) s  … HTU1) /2 width=1 by ldrop_skip/ -L -U1 #T #HTU #HT1
+  elim (lift_div_le … HU2 … HTU) -U /3 width=6 by cpr_zeta, ex2_intro/
+| #G #L #V #U1 #U2 #_ #IHU12 #K #s #d #e #HLK #X #H
   elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
-  elim (IHU12 … HLK … HTU1) -L -U1 /3 width=3/
-| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #K #d #e #HLK #X #HX
+  elim (IHU12 … HLK … HTU1) -L -U1 /3 width=3 by cpr_tau, ex2_intro/
+| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #K #s #d #e #HLK #X #HX
   elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct
   elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct
-  elim (IHV12 … HLK … HV01) -V1 #V3 #HV32 #HV03
-  elim (IHT12 (K.ⓛW0) … HT01) -T1 /2 width=1/ #T3 #HT32 #HT03
-  elim (IHW12 … HLK … HW01) -W1 #W3 #HW32 #HW03
-  @ex2_intro [2: /3 width=2/ | skip |3: /2 width=1/ ] (**) (* /4 width=6/ is slow *)
-| #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #K #d #e #HLK #X #HX
+  elim (IHV12 … HLK … HV01) -V1
+  elim (IHT12 (K.ⓛW0) s … HT01) -T1 /2 width=1 by ldrop_skip/
+  elim (IHW12 … HLK … HW01) -W1 /4 width=7 by cpr_beta, lift_flat, lift_bind, ex2_intro/
+| #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #K #s #d #e #HLK #X #HX
   elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct
   elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct
   elim (IHV1 … HLK … HV01) -V1 #V3 #HV3 #HV03
-  elim (IHT12 (K.ⓓW0) … HT01) -T1 /2 width=1/ #T3 #HT32 #HT03
-  elim (IHW12 … HLK … HW01) -W1 #W3 #HW32 #HW03
-  elim (lift_trans_le … HV3 … HV2) -V // #V #HV3 #HV2
-  @ex2_intro [2: /3 width=2/ | skip |3: /2 width=3/ ] (**) (* /4 width=5/ is slow *)
+  elim (IHT12 (K.ⓓW0) s … HT01) -T1 /2 width=1 by ldrop_skip/ #T3 #HT32 #HT03
+  elim (IHW12 … HLK … HW01) -W1
+  elim (lift_trans_le … HV3 … HV2) -V
+  /4 width=9 by cpr_theta, lift_flat, lift_bind, ex2_intro/
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma
index 0f015cc32..7b99bd8de 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma
@@ -23,8 +23,8 @@ inductive cpx (h) (g): relation4 genv lenv term term ≝
 | cpx_atom : ∀I,G,L. cpx h g G L (⓪{I}) (⓪{I})
 | cpx_sort : ∀G,L,k,l. deg h g k (l+1) → cpx h g G L (⋆k) (⋆(next h k))
 | cpx_delta: ∀I,G,L,K,V,V2,W2,i.
-             ⇩[0, i] L ≡ K.ⓑ{I}V → cpx h g G K V V2 →
-             ⇧[0, i + 1] V2 ≡ W2 → cpx h g G L (#i) W2
+             ⇩[i] L ≡ K.ⓑ{I}V → cpx h g G K V V2 →
+             ⇧[0, i+1] V2 ≡ W2 → cpx h g G L (#i) W2
 | cpx_bind : ∀a,I,G,L,V1,V2,T1,T2.
              cpx h g G L V1 V2 → cpx h g G (L.ⓑ{I}V1) T1 T2 →
              cpx h g G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
@@ -55,7 +55,7 @@ lemma lsubr_cpx_trans: ∀h,g,G. lsub_trans … (cpx h g G) lsubr.
 [ //
 | /2 width=2 by cpx_sort/
 | #I #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
-  elim (lsubr_fwd_drop2_bind … HL12 … HLK1) -HL12 -HLK1 *
+  elim (lsubr_fwd_ldrop2_bind … HL12 … HLK1) -HL12 -HLK1 *
   /4 width=7 by cpx_delta, cpx_ti/
 |4,9: /4 width=1 by cpx_bind, cpx_beta, lsubr_bind/
 |5,7,8: /3 width=1 by cpx_flat, cpx_tau, cpx_ti/
@@ -78,7 +78,7 @@ lemma cpx_pair_sn: ∀h,g,I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡[h, g] V2 →
 #h #g * /2 width=1 by cpx_bind, cpx_flat/
 qed.
 
-lemma cpx_delift: ∀h,g,I,G,K,V,T1,L,d. ⇩[0, d] L ≡ (K.ⓑ{I}V) →
+lemma cpx_delift: ∀h,g,I,G,K,V,T1,L,d. ⇩[d] L ≡ (K.ⓑ{I}V) →
                   ∃∃T2,T.  ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 & ⇧[d, 1] T ≡ T2.
 #h #g #I #G #K #V #T1 elim T1 -T1
 [ * #i #L #d /2 width=4 by cpx_atom, lift_sort, lift_gref, ex2_2_intro/
@@ -108,8 +108,8 @@ qed.
 fact cpx_inv_atom1_aux: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → ∀J. T1 = ⓪{J} →
                         ∨∨ T2 = ⓪{J}
                          | ∃∃k,l. deg h g k (l+1) & T2 = ⋆(next h k) & J = Sort k
-                         | ∃∃I,K,V,V2,i. ⇩[O, i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ➡[h, g] V2 &
-                                         ⇧[O, i + 1] V2 ≡ T2 & J = LRef i.
+                         | ∃∃I,K,V,V2,i. ⇩[i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ➡[h, g] V2 &
+                                         ⇧[O, i+1] V2 ≡ T2 & J = LRef i.
 #G #h #g #L #T1 #T2 * -L -T1 -T2
 [ #I #G #L #J #H destruct /2 width=1 by or3_intro0/
 | #G #L #k #l #Hkl #J #H destruct /3 width=5 by or3_intro1, ex3_2_intro/
@@ -127,8 +127,8 @@ qed-.
 lemma cpx_inv_atom1: ∀h,g,J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ➡[h, g] T2 →
                      ∨∨ T2 = ⓪{J}
                       | ∃∃k,l. deg h g k (l+1) & T2 = ⋆(next h k) & J = Sort k
-                      | ∃∃I,K,V,V2,i. ⇩[O, i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ➡[h, g] V2 &
-                                      ⇧[O, i + 1] V2 ≡ T2 & J = LRef i.
+                      | ∃∃I,K,V,V2,i. ⇩[i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ➡[h, g] V2 &
+                                      ⇧[O, i+1] V2 ≡ T2 & J = LRef i.
 /2 width=3 by cpx_inv_atom1_aux/ qed-.
 
 lemma cpx_inv_sort1: ∀h,g,G,L,T2,k. ⦃G, L⦄ ⊢ ⋆k ➡[h, g] T2 → T2 = ⋆k ∨
@@ -142,8 +142,8 @@ qed-.
 
 lemma cpx_inv_lref1: ∀h,g,G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡[h, g] T2 →
                      T2 = #i ∨
-                     ∃∃I,K,V,V2. ⇩[O, i] L ≡ K. ⓑ{I}V & ⦃G, K⦄ ⊢ V ➡[h, g] V2 &
-                                 ⇧[O, i + 1] V2 ≡ T2.
+                     ∃∃I,K,V,V2. ⇩[i] L ≡ K. ⓑ{I}V & ⦃G, K⦄ ⊢ V ➡[h, g] V2 &
+                                 ⇧[O, i+1] V2 ≡ T2.
 #h #g #G #L #T2 #i #H
 elim (cpx_inv_atom1 … H) -H /2 width=1 by or_introl/ *
 [ #k #l #_ #_ #H destruct
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cpys.ma
new file mode 100644
index 000000000..3c0507b32
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cpys.ma
@@ -0,0 +1,28 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/substitution/cpys_alt.ma".
+include "basic_2/reduction/cpx.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************)
+
+(* Properties on context-sensitive extended multiple substitution for terms *)
+
+lemma cpys_cpx: ∀h,g,G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2.
+#h #g #G #L #T1 #T2 #d #e #H @(cpys_ind_alt … H) -G -L -T1 -T2 -d -e
+/2 width=7 by cpx_delta, cpx_bind, cpx_flat/
+qed.
+
+lemma cpy_cpx: ∀h,g,G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶×[d, e] T2 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2.
+/3 width=3 by cpy_cpys, cpys_cpx/ qed.
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 4da4e21c8..d43413c97 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
@@ -41,56 +41,57 @@ qed.
 
 lemma cpx_lift: ∀h,g,G. l_liftable (cpx h g G).
 #h #g #G #K #T1 #T2 #H elim H -G -K -T1 -T2
-[ #I #G #K #L #d #e #_ #U1 #H1 #U2 #H2
+[ #I #G #K #L #s #d #e #_ #U1 #H1 #U2 #H2
   >(lift_mono … H1 … H2) -H1 -H2 //
-| #G #K #k #l #Hkl #L #d #e #_ #U1 #H1 #U2 #H2
+| #G #K #k #l #Hkl #L #s #d #e #_ #U1 #H1 #U2 #H2
   >(lift_inv_sort1 … H1) -U1
   >(lift_inv_sort1 … H2) -U2 /2 width=2 by cpx_sort/
-| #I #G #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #d #e #HLK #U1 #H #U2 #HWU2
+| #I #G #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #s #d #e #HLK #U1 #H #U2 #HWU2
   elim (lift_inv_lref1 … H) * #Hid #H destruct
   [ elim (lift_trans_ge … HVW2 … HWU2) -W2 // <minus_plus #W2 #HVW2 #HWU2
     elim (ldrop_trans_le … HLK … HKV) -K /2 width=2 by lt_to_le/ #X #HLK #H
-    elim (ldrop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hid #K #Y #HKV #HVY #H destruct /3 width=9 by cpx_delta/
+    elim (ldrop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hid
+    #K #Y #HKV #HVY #H destruct /3 width=10 by cpx_delta/
   | lapply (lift_trans_be … HVW2 … HWU2 ? ?) -W2 /2 width=1 by le_S/ >plus_plus_comm_23 #HVU2
-    lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K /3 width=7 by cpx_delta/
+    lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K /3 width=7 by cpx_delta, ldrop_inv_gen/
   ]
-| #a #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2
+| #a #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #s #d #e #HLK #U1 #H1 #U2 #H2
   elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct
-  elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /4 width=5 by cpx_bind, ldrop_skip/
-| #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2
+  elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /4 width=6 by cpx_bind, ldrop_skip/
+| #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #s #d #e #HLK #U1 #H1 #U2 #H2
   elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct
   elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /3 width=6 by cpx_flat/
-| #G #K #V #T1 #T #T2 #_ #HT2 #IHT1 #L #d #e #HLK #U1 #H #U2 #HTU2
+| #G #K #V #T1 #T #T2 #_ #HT2 #IHT1 #L #s #d #e #HLK #U1 #H #U2 #HTU2
   elim (lift_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct
-  elim (lift_conf_O1 … HTU2 … HT2) -T2 /4 width=5 by cpx_zeta, ldrop_skip/
-| #G #K #V #T1 #T2 #_ #IHT12 #L #d #e #HLK #U1 #H #U2 #HTU2
-  elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=5 by cpx_tau/
-| #G #K #V1 #V2 #T #_ #IHV12 #L #d #e #HLK #U1 #H #U2 #HVU2
-  elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=5 by cpx_ti/
-| #a #G #K #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L #d #e #HLK #X1 #HX1 #X2 #HX2
+  elim (lift_conf_O1 … HTU2 … HT2) -T2 /4 width=6 by cpx_zeta, ldrop_skip/
+| #G #K #V #T1 #T2 #_ #IHT12 #L #s #d #e #HLK #U1 #H #U2 #HTU2
+  elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=6 by cpx_tau/
+| #G #K #V1 #V2 #T #_ #IHV12 #L #s #d #e #HLK #U1 #H #U2 #HVU2
+  elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=6 by cpx_ti/
+| #a #G #K #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L #s #d #e #HLK #X1 #HX1 #X2 #HX2
   elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct
   elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct
   elim (lift_inv_bind1 … HX2) -HX2 #X #T3 #HX #HT23 #HX2 destruct
-  elim (lift_inv_flat1 … HX) -HX #W3 #V3 #HW23 #HV23 #HX destruct /4 width=5 by cpx_beta, ldrop_skip/
-| #a #G #K #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L #d #e #HLK #X1 #HX1 #X2 #HX2
+  elim (lift_inv_flat1 … HX) -HX #W3 #V3 #HW23 #HV23 #HX destruct /4 width=6 by cpx_beta, ldrop_skip/
+| #a #G #K #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L #s #d #e #HLK #X1 #HX1 #X2 #HX2
   elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct
   elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct
   elim (lift_inv_bind1 … HX2) -HX2 #W3 #X #HW23 #HX #HX2 destruct
   elim (lift_inv_flat1 … HX) -HX #V3 #T3 #HV3 #HT23 #HX destruct
-  elim (lift_trans_ge … HV2 … HV3) -V2 /4 width=5 by cpx_theta, ldrop_skip/
+  elim (lift_trans_ge … HV2 … HV3) -V2 /4 width=6 by cpx_theta, ldrop_skip/
 ]
 qed.
 
 lemma cpx_inv_lift1: ∀h,g,G. l_deliftable_sn (cpx h g G).
 #h #g #G #L #U1 #U2 #H elim H -G -L -U1 -U2
-[ * #G #L #i #K #d #e #_ #T1 #H
+[ * #G #L #i #K #s #d #e #_ #T1 #H
   [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by cpx_atom, lift_sort, ex2_intro/
   | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by cpx_atom, lift_lref_ge_minus, lift_lref_lt, ex2_intro/
   | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by cpx_atom, lift_gref, ex2_intro/
   ]
-| #G #L #k #l #Hkl #K #d #e #_ #T1 #H
+| #G #L #k #l #Hkl #K #s #d #e #_ #T1 #H
   lapply (lift_inv_sort2 … H) -H #H destruct /3 width=3 by cpx_sort, lift_sort, ex2_intro/
-| #I #G #L #LV #V #V2 #W2 #i #HLV #HV2 #HVW2 #IHV2 #K #d #e #HLK #T1 #H
+| #I #G #L #LV #V #V2 #W2 #i #HLV #HV2 #HVW2 #IHV2 #K #s #d #e #HLK #T1 #H
   elim (lift_inv_lref2 … H) -H * #Hid #H destruct
   [ elim (ldrop_conf_lt … HLK … HLV) -L // #L #U #HKL #HLV #HUV
     elim (IHV2 … HLV … HUV) -V #U2 #HUV2 #HU2
@@ -100,36 +101,36 @@ lemma cpx_inv_lift1: ∀h,g,G. l_deliftable_sn (cpx h g G).
     elim (lift_split … HVW2 d (i - e + 1)) -HVW2 /3 width=1 by le_S, le_S_S/ -Hid -Hdie
     #V1 #HV1 >plus_minus // <minus_minus /2 width=1 by le_S/ <minus_n_n <plus_n_O /3 width=9 by cpx_delta, ex2_intro/
   ]
-| #a #I #G #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H
+| #a #I #G #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #s #d #e #HLK #X #H
   elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
   elim (IHV12 … HLK … HWV1) -IHV12 #W2 #HW12 #HWV2
-  elim (IHU12 … HTU1) -IHU12 -HTU1 /3 width=5 by cpx_bind, ldrop_skip, lift_bind, ex2_intro/
-| #I #G #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H
+  elim (IHU12 … HTU1) -IHU12 -HTU1 /3 width=6 by cpx_bind, ldrop_skip, lift_bind, ex2_intro/
+| #I #G #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #s #d #e #HLK #X #H
   elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
   elim (IHV12 … HLK … HWV1) -V1
   elim (IHU12 … HLK … HTU1) -U1 -HLK /3 width=5 by cpx_flat, lift_flat, ex2_intro/
-| #G #L #V #U1 #U #U2 #_ #HU2 #IHU1 #K #d #e #HLK #X #H
+| #G #L #V #U1 #U #U2 #_ #HU2 #IHU1 #K #s #d #e #HLK #X #H
   elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
-  elim (IHU1 (K.ⓓW1) … HTU1) /2 width=1/ -L -U1 #T #HTU #HT1
+  elim (IHU1 (K.ⓓW1) s … HTU1) /2 width=1/ -L -U1 #T #HTU #HT1
   elim (lift_div_le … HU2 … HTU) -U /3 width=5 by cpx_zeta, ex2_intro/
-| #G #L #V #U1 #U2 #_ #IHU12 #K #d #e #HLK #X #H
+| #G #L #V #U1 #U2 #_ #IHU12 #K #s #d #e #HLK #X #H
   elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
   elim (IHU12 … HLK … HTU1) -L -U1 /3 width=3 by cpx_tau, ex2_intro/
-| #G #L #V1 #V2 #U1 #_ #IHV12 #K #d #e #HLK #X #H
+| #G #L #V1 #V2 #U1 #_ #IHV12 #K #s #d #e #HLK #X #H
   elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
   elim (IHV12 … HLK … HWV1) -L -V1 /3 width=3 by cpx_ti, ex2_intro/
-| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #K #d #e #HLK #X #HX
+| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #K #s #d #e #HLK #X #HX
   elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct
   elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct
   elim (IHV12 … HLK … HV01) -V1 #V3 #HV32 #HV03
-  elim (IHT12 (K.ⓛW0) … HT01) -T1 /2 width=1 by ldrop_skip/ #T3 #HT32 #HT03
+  elim (IHT12 (K.ⓛW0) s … HT01) -T1 /2 width=1 by ldrop_skip/ #T3 #HT32 #HT03
   elim (IHW12 … HLK … HW01) -W1
   /4 width=7 by cpx_beta, lift_bind, lift_flat, ex2_intro/
-| #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #K #d #e #HLK #X #HX
+| #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #K #s #d #e #HLK #X #HX
   elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct
   elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct
   elim (IHV1 … HLK … HV01) -V1 #V3 #HV3 #HV03
-  elim (IHT12 (K.ⓓW0) … HT01) -T1 /2 width=1 by ldrop_skip/ #T3 #HT32 #HT03
+  elim (IHT12 (K.ⓓW0) s … HT01) -T1 /2 width=1 by ldrop_skip/ #T3 #HT32 #HT03
   elim (IHW12 … HLK … HW01) -W1 #W3 #HW32 #HW03
   elim (lift_trans_le … HV3 … HV2) -V
   /4 width=9 by cpx_theta, lift_bind, lift_flat, ex2_intro/
@@ -217,7 +218,7 @@ lemma fqu_cpx_trans_neq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L
   ]
 | #G #L #K #T1 #U1 #e #HLK #HTU1 #T2 #HT12 #H elim (lift_total T2 0 (e+1))
   #U2 #HTU2 @(ex3_intro … U2)
-  [1,3: /2 width=9 by cpx_lift, fqu_drop/
+  [1,3: /2 width=10 by cpx_lift, fqu_drop/
   | #H0 destruct /3 width=5 by lift_inj/
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/crr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/crr.ma
index 01ed1dbab..79d9269b3 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/crr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/crr.ma
@@ -29,7 +29,7 @@ definition ib2: relation2 bool bind2 ≝
 (* activate genv *)
 (* reducible terms *)
 inductive crr (G:genv): relation2 lenv term ≝
-| crr_delta  : ∀L,K,V,i. ⇩[0, i] L ≡ K.ⓓV → crr G L (#i)
+| crr_delta  : ∀L,K,V,i. ⇩[i] L ≡ K.ⓓV → crr G L (#i)
 | crr_appl_sn: ∀L,V,T. crr G L V → crr G L (ⓐV.T)
 | crr_appl_dx: ∀L,V,T. crr G L T → crr G L (ⓐV.T)
 | crr_ri2    : ∀I,L,V,T. ri2 I → crr G L (②{I}V.T)
@@ -62,9 +62,9 @@ lemma crr_inv_sort: ∀G,L,k. ⦃G, L⦄ ⊢ 𝐑⦃⋆k⦄ → ⊥.
 /2 width=6 by crr_inv_sort_aux/ qed-.
 
 fact crr_inv_lref_aux: ∀G,L,T,i. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → T = #i →
-                       ∃∃K,V. ⇩[0, i] L ≡ K.ⓓV.
+                       ∃∃K,V. ⇩[i] L ≡ K.ⓓV.
 #G #L #T #j * -L -T
-[ #L #K #V #i #HLK #H destruct /2 width=3/
+[ #L #K #V #i #HLK #H destruct /2 width=3 by ex1_2_intro/
 | #L #V #T #_ #H destruct
 | #L #V #T #_ #H destruct
 | #I #L #V #T #_ #H destruct
@@ -75,7 +75,7 @@ fact crr_inv_lref_aux: ∀G,L,T,i. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → T = #i →
 ]
 qed-.
 
-lemma crr_inv_lref: ∀G,L,i. ⦃G, L⦄ ⊢ 𝐑⦃#i⦄ → ∃∃K,V. ⇩[0, i] L ≡ K.ⓓV.
+lemma crr_inv_lref: ∀G,L,i. ⦃G, L⦄ ⊢ 𝐑⦃#i⦄ → ∃∃K,V. ⇩[i] L ≡ K.ⓓV.
 /2 width=4 by crr_inv_lref_aux/ qed-.
 
 fact crr_inv_gref_aux: ∀G,L,T,p. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → T = §p → ⊥.
@@ -112,8 +112,8 @@ fact crr_inv_ib2_aux: ∀a,I,G,L,W,U,T. ib2 a I → ⦃G, L⦄ ⊢ 𝐑⦃T⦄ 
 | #I #L #V #T #H1 #H2 destruct
   elim H1 -H1 #H destruct
   elim HI -HI #H destruct
-| #a #I #L #V #T #_ #HV #H destruct /2 width=1/
-| #a #I #L #V #T #_ #HT #H destruct /2 width=1/
+| #a #I #L #V #T #_ #HV #H destruct /2 width=1 by or_introl/
+| #a #I #L #V #T #_ #HT #H destruct /2 width=1 by or_intror/
 | #a #L #V #W #T #H destruct
 | #a #L #V #W #T #H destruct
 ]
@@ -127,8 +127,8 @@ fact crr_inv_appl_aux: ∀G,L,W,U,T. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → T = ⓐW.U 
                        ∨∨ ⦃G, L⦄ ⊢ 𝐑⦃W⦄ | ⦃G, L⦄ ⊢ 𝐑⦃U⦄ | (𝐒⦃U⦄ → ⊥).
 #G #L #W0 #U #T * -L -T
 [ #L #K #V #i #_ #H destruct
-| #L #V #T #HV #H destruct /2 width=1/
-| #L #V #T #HT #H destruct /2 width=1/
+| #L #V #T #HV #H destruct /2 width=1 by or3_intro0/
+| #L #V #T #HT #H destruct /2 width=1 by or3_intro1/
 | #I #L #V #T #H1 #H2 destruct
   elim H1 -H1 #H destruct
 | #a #I #L #V #T #_ #_ #H destruct
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_lift.ma
index d64a17d4c..4b28fc1dc 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_lift.ma
@@ -19,56 +19,56 @@ include "basic_2/reduction/crr.ma".
 
 (* Properties on relocation *************************************************)
 
-lemma crr_lift: ∀G,K,T. ⦃G, K⦄ ⊢ 𝐑⦃T⦄ → ∀L,d,e. ⇩[d, e] L ≡ K →
+lemma crr_lift: ∀G,K,T. ⦃G, K⦄ ⊢ 𝐑⦃T⦄ → ∀L,s,d,e. ⇩[s, d, e] L ≡ K →
                 ∀U. ⇧[d, e] T ≡ U → ⦃G, L⦄ ⊢ 𝐑⦃U⦄.
 #G #K #T #H elim H -K -T
-[ #K #K0 #V #i #HK0 #L #d #e #HLK #X #H
+[ #K #K0 #V #i #HK0 #L #s #d #e #HLK #X #H
   elim (lift_inv_lref1 … H) -H * #Hid #H destruct
-  [ elim (ldrop_trans_lt … HLK … HK0) -K // /2 width=4/
-  | lapply (ldrop_trans_ge … HLK … HK0 ?) -K // /2 width=4/
+  [ elim (ldrop_trans_lt … HLK … HK0) -K /2 width=4 by crr_delta/
+  | lapply (ldrop_trans_ge … HLK … HK0 ?) -K /3 width=4 by crr_delta, ldrop_inv_gen/
   ]
-| #K #V #T #_ #IHV #L #d #e #HLK #X #H
-  elim (lift_inv_flat1 … H) -H #W #U #HVW #_ #H destruct /3 width=4/
-| #K #V #T #_ #IHT #L #d #e #HLK #X #H
-  elim (lift_inv_flat1 … H) -H #W #U #_ #HTU #H destruct /3 width=4/
-| #I #K #V #T #HI #L #d #e #_ #X #H
-  elim (lift_fwd_pair1 … H) -H #W #U #_ #H destruct /2 width=1/
-| #a #I #K #V #T #HI #_ #IHV #L #d #e #HLK #X #H
-  elim (lift_inv_bind1 … H) -H #W #U #HVW #_ #H destruct /3 width=4/
-| #a #I #K #V #T #HI #_ #IHT #L #d #e #HLK #X #H
-  elim (lift_inv_bind1 … H) -H #W #U #HVW #HTU #H destruct /4 width=4/
-| #a #K #V #V0 #T #L #d #e #_ #X #H
+| #K #V #T #_ #IHV #L #s #d #e #HLK #X #H
+  elim (lift_inv_flat1 … H) -H #W #U #HVW #_ #H destruct /3 width=5 by crr_appl_sn/
+| #K #V #T #_ #IHT #L #s #d #e #HLK #X #H
+  elim (lift_inv_flat1 … H) -H #W #U #_ #HTU #H destruct /3 width=5 by crr_appl_dx/
+| #I #K #V #T #HI #L #s #d #e #_ #X #H
+  elim (lift_fwd_pair1 … H) -H #W #U #_ #H destruct /2 width=1 by crr_ri2/
+| #a #I #K #V #T #HI #_ #IHV #L #s #d #e #HLK #X #H
+  elim (lift_inv_bind1 … H) -H #W #U #HVW #_ #H destruct /3 width=5 by crr_ib2_sn/
+| #a #I #K #V #T #HI #_ #IHT #L #s #d #e #HLK #X #H
+  elim (lift_inv_bind1 … H) -H #W #U #HVW #HTU #H destruct /4 width=5 by crr_ib2_dx, ldrop_skip/
+| #a #K #V #V0 #T #L #s #d #e #_ #X #H
   elim (lift_inv_flat1 … H) -H #W #X0 #_ #H0 #H destruct
-  elim (lift_inv_bind1 … H0) -H0 #W0 #U #_ #_ #H0 destruct /2 width=1/
-| #a #K #V #V0 #T #L #d #e #_ #X #H
+  elim (lift_inv_bind1 … H0) -H0 #W0 #U #_ #_ #H0 destruct /2 width=1 by crr_beta/
+| #a #K #V #V0 #T #L #s #d #e #_ #X #H
   elim (lift_inv_flat1 … H) -H #W #X0 #_ #H0 #H destruct
-  elim (lift_inv_bind1 … H0) -H0 #W0 #U #_ #_ #H0 destruct /2 width=1/
+  elim (lift_inv_bind1 … H0) -H0 #W0 #U #_ #_ #H0 destruct /2 width=1 by crr_theta/
 ]
 qed.
 
-lemma crr_inv_lift: ∀G,L,U. ⦃G, L⦄ ⊢ 𝐑⦃U⦄ → ∀K,d,e. ⇩[d, e] L ≡ K →
+lemma crr_inv_lift: ∀G,L,U. ⦃G, L⦄ ⊢ 𝐑⦃U⦄ → ∀K,s,d,e. ⇩[s, d, e] L ≡ K →
                     ∀T. ⇧[d, e] T ≡ U → ⦃G, K⦄ ⊢ 𝐑⦃T⦄.
 #G #L #U #H elim H -L -U
-[ #L #L0 #W #i #HK0 #K #d #e #HLK #X #H
+[ #L #L0 #W #i #HK0 #K #s #d #e #HLK #X #H
   elim (lift_inv_lref2 … H) -H * #Hid #H destruct
-  [ elim (ldrop_conf_lt … HLK … HK0) -L // /2 width=4/
-  | lapply (ldrop_conf_ge … HLK … HK0 ?) -L // /2 width=4/
+  [ elim (ldrop_conf_lt … HLK … HK0) -L /2 width=4 by crr_delta/
+  | lapply (ldrop_conf_ge … HLK … HK0 ?) -L /2 width=4 by crr_delta/
   ]
-| #L #W #U #_ #IHW #K #d #e #HLK #X #H
-  elim (lift_inv_flat2 … H) -H #V #T #HVW #_ #H destruct /3 width=4/
-| #L #W #U #_ #IHU #K #d #e #HLK #X #H
-  elim (lift_inv_flat2 … H) -H #V #T #_ #HTU #H destruct /3 width=4/
-| #I #L #W #U #HI #K #d #e #_ #X #H
-  elim (lift_fwd_pair2 … H) -H #V #T #_ #H destruct /2 width=1/
-| #a #I #L #W #U #HI #_ #IHW #K #d #e #HLK #X #H
-  elim (lift_inv_bind2 … H) -H #V #T #HVW #_ #H destruct /3 width=4/
-| #a #I #L #W #U #HI #_ #IHU #K #d #e #HLK #X #H
-  elim (lift_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct /4 width=4/
-| #a #L #W #W0 #U #K #d #e #_ #X #H
+| #L #W #U #_ #IHW #K #s #d #e #HLK #X #H
+  elim (lift_inv_flat2 … H) -H #V #T #HVW #_ #H destruct /3 width=5 by crr_appl_sn/
+| #L #W #U #_ #IHU #K #s #d #e #HLK #X #H
+  elim (lift_inv_flat2 … H) -H #V #T #_ #HTU #H destruct /3 width=5 by crr_appl_dx/
+| #I #L #W #U #HI #K #s #d #e #_ #X #H
+  elim (lift_fwd_pair2 … H) -H #V #T #_ #H destruct /2 width=1 by crr_ri2/
+| #a #I #L #W #U #HI #_ #IHW #K #s #d #e #HLK #X #H
+  elim (lift_inv_bind2 … H) -H #V #T #HVW #_ #H destruct /3 width=5 by crr_ib2_sn/
+| #a #I #L #W #U #HI #_ #IHU #K #s #d #e #HLK #X #H
+  elim (lift_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct /4 width=5 by crr_ib2_dx, ldrop_skip/
+| #a #L #W #W0 #U #K #s #d #e #_ #X #H
   elim (lift_inv_flat2 … H) -H #V #X0 #_ #H0 #H destruct
-  elim (lift_inv_bind2 … H0) -H0 #V0 #T #_ #_ #H0 destruct /2 width=1/
-| #a #L #W #W0 #U #K #d #e #_ #X #H
+  elim (lift_inv_bind2 … H0) -H0 #V0 #T #_ #_ #H0 destruct /2 width=1 by crr_beta/
+| #a #L #W #W0 #U #K #s #d #e #_ #X #H
   elim (lift_inv_flat2 … H) -H #V #X0 #_ #H0 #H destruct
-  elim (lift_inv_bind2 … H0) -H0 #V0 #T #_ #_ #H0 destruct /2 width=1/
+  elim (lift_inv_bind2 … H0) -H0 #V0 #T #_ #_ #H0 destruct /2 width=1 by crr_theta/
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/crx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/crx.ma
index 6a4cbbb4e..8c26803ad 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/crx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/crx.ma
@@ -22,7 +22,7 @@ include "basic_2/reduction/crr.ma".
 (* extended reducible terms *)
 inductive crx (h) (g) (G:genv): relation2 lenv term ≝
 | crx_sort   : ∀L,k,l. deg h g k (l+1) → crx h g G L (⋆k)
-| crx_delta  : ∀I,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → crx h g G L (#i)
+| crx_delta  : ∀I,L,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → crx h g G L (#i)
 | crx_appl_sn: ∀L,V,T. crx h g G L V → crx h g G L (ⓐV.T)
 | crx_appl_dx: ∀L,V,T. crx h g G L T → crx h g G L (ⓐV.T)
 | crx_ri2    : ∀I,L,V,T. ri2 I → crx h g G L (②{I}V.T)
@@ -39,7 +39,8 @@ interpretation
 (* Basic properties *********************************************************)
 
 lemma crr_crx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄.
-#h #g #G #L #T #H elim H -L -T // /2 width=1/ /2 width=4/
+#h #g #G #L #T #H elim H -L -T
+/2 width=4 by crx_delta, crx_appl_sn, crx_appl_dx, crx_ri2, crx_ib2_sn, crx_ib2_dx, crx_beta, crx_theta/
 qed.
 
 (* Basic inversion lemmas ***************************************************)
@@ -47,7 +48,7 @@ qed.
 fact crx_inv_sort_aux: ∀h,g,G,L,T,k. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → T = ⋆k →
                        ∃l. deg h g k (l+1).
 #h #g #G #L #T #k0 * -L -T
-[ #L #k #l #Hkl #H destruct /2 width=2/
+[ #L #k #l #Hkl #H destruct /2 width=2 by ex_intro/
 | #I #L #K #V #i #HLK #H destruct
 | #L #V #T #_ #H destruct
 | #L #V #T #_ #H destruct
@@ -63,10 +64,10 @@ lemma crx_inv_sort: ∀h,g,G,L,k. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃⋆k⦄ → ∃l.
 /2 width=5 by crx_inv_sort_aux/ qed-.
 
 fact crx_inv_lref_aux: ∀h,g,G,L,T,i. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → T = #i →
-                       ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V.
+                       ∃∃I,K,V. ⇩[i] L ≡ K.ⓑ{I}V.
 #h #g #G #L #T #j * -L -T
 [ #L #k #l #_ #H destruct
-| #I #L #K #V #i #HLK #H destruct /2 width=4/
+| #I #L #K #V #i #HLK #H destruct /2 width=4 by ex1_3_intro/
 | #L #V #T #_ #H destruct
 | #L #V #T #_ #H destruct
 | #I #L #V #T #_ #H destruct
@@ -77,7 +78,7 @@ fact crx_inv_lref_aux: ∀h,g,G,L,T,i. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → T =
 ]
 qed-.
 
-lemma crx_inv_lref: ∀h,g,G,L,i. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃#i⦄ → ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V.
+lemma crx_inv_lref: ∀h,g,G,L,i. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃#i⦄ → ∃∃I,K,V. ⇩[i] L ≡ K.ⓑ{I}V.
 /2 width=6 by crx_inv_lref_aux/ qed-.
 
 fact crx_inv_gref_aux: ∀h,g,G,L,T,p. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → T = §p → ⊥.
@@ -100,7 +101,7 @@ lemma crx_inv_gref: ∀h,g,G,L,p. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃§p⦄ → ⊥.
 lemma trx_inv_atom: ∀h,g,I,G. ⦃G, ⋆⦄ ⊢ 𝐑[h, g]⦃⓪{I}⦄ →
                     ∃∃k,l. deg h g k (l+1) & I = Sort k.
 #h #g * #i #G #H
-[ elim (crx_inv_sort … H) -H /2 width=4/
+[ elim (crx_inv_sort … H) -H /2 width=4 by ex2_2_intro/
 | elim (crx_inv_lref … H) -H #I #L #V #H
   elim (ldrop_inv_atom1 … H) -H #H destruct
 | elim (crx_inv_gref … H)
@@ -117,8 +118,8 @@ fact crx_inv_ib2_aux: ∀h,g,a,I,G,L,W,U,T. ib2 a I → ⦃G, L⦄ ⊢ 𝐑[h, g
 | #I #L #V #T #H1 #H2 destruct
   elim H1 -H1 #H destruct
   elim HI -HI #H destruct
-| #a #I #L #V #T #_ #HV #H destruct /2 width=1/
-| #a #I #L #V #T #_ #HT #H destruct /2 width=1/
+| #a #I #L #V #T #_ #HV #H destruct /2 width=1 by or_introl/
+| #a #I #L #V #T #_ #HT #H destruct /2 width=1 by or_intror/
 | #a #L #V #W #T #H destruct
 | #a #L #V #W #T #H destruct
 ]
@@ -133,8 +134,8 @@ fact crx_inv_appl_aux: ∀h,g,G,L,W,U,T. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → T
 #h #g #G #L #W0 #U #T * -L -T
 [ #L #k #l #_ #H destruct
 | #I #L #K #V #i #_ #H destruct
-| #L #V #T #HV #H destruct /2 width=1/
-| #L #V #T #HT #H destruct /2 width=1/
+| #L #V #T #HV #H destruct /2 width=1 by or3_intro0/
+| #L #V #T #HT #H destruct /2 width=1 by or3_intro1/
 | #I #L #V #T #H1 #H2 destruct
   elim H1 -H1 #H destruct
 | #a #I #L #V #T #_ #_ #H destruct
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_lift.ma
index c4902bb35..9e1bc9f81 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_lift.ma
@@ -19,60 +19,60 @@ include "basic_2/reduction/crx.ma".
 
 (* Properties on relocation *************************************************)
 
-lemma crx_lift: ∀h,g,G,K,T. ⦃G, K⦄ ⊢ 𝐑[h, g]⦃T⦄ → ∀L,d,e. ⇩[d, e] L ≡ K →
+lemma crx_lift: ∀h,g,G,K,T. ⦃G, K⦄ ⊢ 𝐑[h, g]⦃T⦄ → ∀L,s,d,e. ⇩[s, d, e] L ≡ K →
                 ∀U. ⇧[d, e] T ≡ U → ⦃G, L⦄ ⊢ 𝐑[h, g]⦃U⦄.
 #h #g #G #K #T #H elim H -K -T
-[ #K #k #l #Hkl #L #d #e #_ #X #H
-  >(lift_inv_sort1 … H) -X /2 width=2/
-| #I #K #K0 #V #i #HK0 #L #d #e #HLK #X #H
+[ #K #k #l #Hkl #L #s #d #e #_ #X #H
+  >(lift_inv_sort1 … H) -X /2 width=2 by crx_sort/
+| #I #K #K0 #V #i #HK0 #L #s #d #e #HLK #X #H
   elim (lift_inv_lref1 … H) -H * #Hid #H destruct
-  [ elim (ldrop_trans_lt … HLK … HK0) -K // /2 width=4/
-  | lapply (ldrop_trans_ge … HLK … HK0 ?) -K // /2 width=4/
+  [ elim (ldrop_trans_lt … HLK … HK0) -K /2 width=4 by crx_delta/
+  | lapply (ldrop_trans_ge … HLK … HK0 ?) -K /3 width=5 by crx_delta, ldrop_inv_gen/
   ]
-| #K #V #T #_ #IHV #L #d #e #HLK #X #H
-  elim (lift_inv_flat1 … H) -H #W #U #HVW #_ #H destruct /3 width=4/
-| #K #V #T #_ #IHT #L #d #e #HLK #X #H
-  elim (lift_inv_flat1 … H) -H #W #U #_ #HTU #H destruct /3 width=4/
-| #I #K #V #T #HI #L #d #e #_ #X #H
-  elim (lift_fwd_pair1 … H) -H #W #U #_ #H destruct /2 width=1/
-| #a #I #K #V #T #HI #_ #IHV #L #d #e #HLK #X #H
-  elim (lift_inv_bind1 … H) -H #W #U #HVW #_ #H destruct /3 width=4/
-| #a #I #K #V #T #HI #_ #IHT #L #d #e #HLK #X #H
-  elim (lift_inv_bind1 … H) -H #W #U #HVW #HTU #H destruct /4 width=4/
-| #a #K #V #V0 #T #L #d #e #_ #X #H
+| #K #V #T #_ #IHV #L #s #d #e #HLK #X #H
+  elim (lift_inv_flat1 … H) -H #W #U #HVW #_ #H destruct /3 width=5 by crx_appl_sn/
+| #K #V #T #_ #IHT #L #s #d #e #HLK #X #H
+  elim (lift_inv_flat1 … H) -H #W #U #_ #HTU #H destruct /3 width=5 by crx_appl_dx/
+| #I #K #V #T #HI #L #s #d #e #_ #X #H
+  elim (lift_fwd_pair1 … H) -H #W #U #_ #H destruct /2 width=1 by crx_ri2/
+| #a #I #K #V #T #HI #_ #IHV #L #s #d #e #HLK #X #H
+  elim (lift_inv_bind1 … H) -H #W #U #HVW #_ #H destruct /3 width=5 by crx_ib2_sn/
+| #a #I #K #V #T #HI #_ #IHT #L #s #d #e #HLK #X #H
+  elim (lift_inv_bind1 … H) -H #W #U #HVW #HTU #H destruct /4 width=5 by crx_ib2_dx, ldrop_skip/
+| #a #K #V #V0 #T #L #s #d #e #_ #X #H
   elim (lift_inv_flat1 … H) -H #W #X0 #_ #H0 #H destruct
-  elim (lift_inv_bind1 … H0) -H0 #W0 #U #_ #_ #H0 destruct /2 width=1/
-| #a #K #V #V0 #T #L #d #e #_ #X #H
+  elim (lift_inv_bind1 … H0) -H0 #W0 #U #_ #_ #H0 destruct /2 width=1 by crx_beta/
+| #a #K #V #V0 #T #L #s #d #e #_ #X #H
   elim (lift_inv_flat1 … H) -H #W #X0 #_ #H0 #H destruct
-  elim (lift_inv_bind1 … H0) -H0 #W0 #U #_ #_ #H0 destruct /2 width=1/
+  elim (lift_inv_bind1 … H0) -H0 #W0 #U #_ #_ #H0 destruct /2 width=1 by crx_theta/
 ]
 qed.
 
-lemma crx_inv_lift: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃U⦄ → ∀K,d,e. ⇩[d, e] L ≡ K →
+lemma crx_inv_lift: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃U⦄ → ∀K,s,d,e. ⇩[s, d, e] L ≡ K →
                     ∀T. ⇧[d, e] T ≡ U → ⦃G, K⦄ ⊢ 𝐑[h, g]⦃T⦄.
 #h #g #G #L #U #H elim H -L -U
-[ #L #k #l #Hkl #K #d #e #_ #X #H
-  >(lift_inv_sort2 … H) -X /2 width=2/
-| #I #L #L0 #W #i #HK0 #K #d #e #HLK #X #H
+[ #L #k #l #Hkl #K #s #d #e #_ #X #H
+  >(lift_inv_sort2 … H) -X /2 width=2 by crx_sort/
+| #I #L #L0 #W #i #HK0 #K #s #d #e #HLK #X #H
   elim (lift_inv_lref2 … H) -H * #Hid #H destruct
-  [ elim (ldrop_conf_lt … HLK … HK0) -L // /2 width=4/
-  | lapply (ldrop_conf_ge … HLK … HK0 ?) -L // /2 width=4/
+  [ elim (ldrop_conf_lt … HLK … HK0) -L /2 width=4 by crx_delta/
+  | lapply (ldrop_conf_ge … HLK … HK0 ?) -L /2 width=4 by crx_delta/
   ]
-| #L #W #U #_ #IHW #K #d #e #HLK #X #H
-  elim (lift_inv_flat2 … H) -H #V #T #HVW #_ #H destruct /3 width=4/
-| #L #W #U #_ #IHU #K #d #e #HLK #X #H
-  elim (lift_inv_flat2 … H) -H #V #T #_ #HTU #H destruct /3 width=4/
-| #I #L #W #U #HI #K #d #e #_ #X #H
-  elim (lift_fwd_pair2 … H) -H #V #T #_ #H destruct /2 width=1/
-| #a #I #L #W #U #HI #_ #IHW #K #d #e #HLK #X #H
-  elim (lift_inv_bind2 … H) -H #V #T #HVW #_ #H destruct /3 width=4/
-| #a #I #L #W #U #HI #_ #IHU #K #d #e #HLK #X #H
-  elim (lift_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct /4 width=4/
-| #a #L #W #W0 #U #K #d #e #_ #X #H
+| #L #W #U #_ #IHW #K #s #d #e #HLK #X #H
+  elim (lift_inv_flat2 … H) -H #V #T #HVW #_ #H destruct /3 width=5 by crx_appl_sn/
+| #L #W #U #_ #IHU #K #s #d #e #HLK #X #H
+  elim (lift_inv_flat2 … H) -H #V #T #_ #HTU #H destruct /3 width=5 by crx_appl_dx/
+| #I #L #W #U #HI #K #s #d #e #_ #X #H
+  elim (lift_fwd_pair2 … H) -H #V #T #_ #H destruct /2 width=1 by crx_ri2/
+| #a #I #L #W #U #HI #_ #IHW #K #s #d #e #HLK #X #H
+  elim (lift_inv_bind2 … H) -H #V #T #HVW #_ #H destruct /3 width=5 by crx_ib2_sn/
+| #a #I #L #W #U #HI #_ #IHU #K #s #d #e #HLK #X #H
+  elim (lift_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct /4 width=5 by crx_ib2_dx, ldrop_skip/
+| #a #L #W #W0 #U #K #s #d #e #_ #X #H
   elim (lift_inv_flat2 … H) -H #V #X0 #_ #H0 #H destruct
-  elim (lift_inv_bind2 … H0) -H0 #V0 #T #_ #_ #H0 destruct /2 width=1/
-| #a #L #W #W0 #U #K #d #e #_ #X #H
+  elim (lift_inv_bind2 … H0) -H0 #V0 #T #_ #_ #H0 destruct /2 width=1 by crx_beta/
+| #a #L #W #W0 #U #K #s #d #e #_ #X #H
   elim (lift_inv_flat2 … H) -H #V #X0 #_ #H0 #H destruct
-  elim (lift_inv_bind2 … H0) -H0 #V0 #T #_ #_ #H0 destruct /2 width=1/
+  elim (lift_inv_bind2 … H0) -H0 #V0 #T #_ #_ #H0 destruct /2 width=1 by crx_theta/
 ]
-qed.
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma
index 29bc6a975..a0f04dd96 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma
@@ -23,11 +23,11 @@ include "basic_2/reduction/lpr.ma".
 
 (* Basic_1: includes: wcpr0_drop *)
 lemma lpr_ldrop_conf: ∀G. dropable_sn (lpr G).
-/3 width=5 by lpx_sn_deliftable_dropable, cpr_inv_lift1/ qed-.
+/3 width=6 by lpx_sn_deliftable_dropable, cpr_inv_lift1/ qed-.
 
 (* Basic_1: includes: wcpr0_drop_back *)
 lemma ldrop_lpr_trans: ∀G. dedropable_sn (lpr G).
-/3 width=9 by lpx_sn_liftable_dedropable, cpr_lift/ qed-.
+/3 width=10 by lpx_sn_liftable_dedropable, cpr_lift/ qed-.
 
 lemma lpr_ldrop_trans_O1: ∀G. dropable_dx (lpr G).
 /2 width=3 by lpx_sn_dropable/ qed-.
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 fb9e9e691..deaeff927 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma
@@ -31,7 +31,7 @@ fact cpr_conf_lpr_atom_delta:
       ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 →
       ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0
    ) →
-   ∀K0,V0. ⇩[O, i] L0 ≡ K0.ⓓV0 →
+   ∀K0,V0. ⇩[i] L0 ≡ K0.ⓓV0 →
    ∀V2. ⦃G, K0⦄ ⊢ V0 ➡ V2 → ∀T2. ⇧[O, i + 1] V2 ≡ T2 →
    ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡ L2 →
    ∃∃T. ⦃G, L1⦄ ⊢ #i ➡ T & ⦃G, L2⦄ ⊢ T2 ➡ T.
@@ -44,7 +44,7 @@ lapply (ldrop_fwd_drop2 … HLK2) -W2 #HLK2
 lapply (fqup_lref … G … HLK0) -HLK0 #HLK0
 elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2
 elim (lift_total V 0 (i+1))
-/3 width=11 by cpr_lift, cpr_delta, ex2_intro/
+/3 width=12 by cpr_lift, cpr_delta, ex2_intro/
 qed-.
 
 (* Basic_1: includes: pr0_delta_delta pr2_delta_delta *)
@@ -55,9 +55,9 @@ fact cpr_conf_lpr_delta_delta:
       ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 →
       ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0
    ) →
-   ∀K0,V0. ⇩[O, i] L0 ≡ K0.ⓓV0 →
+   ∀K0,V0. ⇩[i] L0 ≡ K0.ⓓV0 →
    ∀V1. ⦃G, K0⦄ ⊢ V0 ➡ V1 → ∀T1. ⇧[O, i + 1] V1 ≡ T1 →
-   ∀KX,VX. ⇩[O, i] L0 ≡ KX.ⓓVX →
+   ∀KX,VX. ⇩[i] L0 ≡ KX.ⓓVX →
    ∀V2. ⦃G, KX⦄ ⊢ VX ➡ V2 → ∀T2. ⇧[O, i + 1] V2 ≡ T2 →
    ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡ L2 →
    ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡ T & ⦃G, L2⦄ ⊢ T2 ➡ T.
@@ -72,7 +72,7 @@ elim (lpr_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct
 lapply (ldrop_fwd_drop2 … HLK2) -W2 #HLK2
 lapply (fqup_lref … G … HLK0) -HLK0 #HLK0
 elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2
-elim (lift_total V 0 (i+1)) /3 width=11 by cpr_lift, ex2_intro/
+elim (lift_total V 0 (i+1)) /3 width=12 by cpr_lift, ex2_intro/
 qed-.
 
 fact cpr_conf_lpr_bind_bind:
@@ -124,8 +124,8 @@ fact cpr_conf_lpr_zeta_zeta:
 #G #L0 #V0 #T0 #IH #T1 #HT01 #X1 #HXT1
 #T2 #HT02 #X2 #HXT2 #L1 #HL01 #L2 #HL02
 elim (IH … HT01 … HT02 (L1.ⓓV0) … (L2.ⓓV0)) -IH -HT01 -HT02 /2 width=1 by lpr_pair/ -L0 -T0 #T #HT1 #HT2
-elim (cpr_inv_lift1 … HT1 L1 … HXT1) -T1 /2 width=1 by ldrop_drop/ #T1 #HT1 #HXT1
-elim (cpr_inv_lift1 … HT2 L2 … HXT2) -T2 /2 width=1 by ldrop_drop/ #T2 #HT2 #HXT2
+elim (cpr_inv_lift1 … HT1 L1 … HXT1) -T1 /2 width=2 by ldrop_drop/ #T1 #HT1 #HXT1
+elim (cpr_inv_lift1 … HT2 L2 … HXT2) -T2 /2 width=2 by ldrop_drop/ #T2 #HT2 #HXT2
 lapply (lift_inj … HT2 … HT1) -T #H destruct /2 width=3 by ex2_intro/
 qed-.
 
@@ -217,7 +217,7 @@ fact cpr_conf_lpr_flat_theta:
 #V2 #HV02 #U2 #HVU2 #W2 #HW02 #T2 #HT02 #L1 #HL01 #L2 #HL02
 elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2
 elim (lift_total V 0 1) #U #HVU
-lapply (cpr_lift … HV2 (L2.ⓓW2) … HVU2 … HVU) -HVU2 /2 width=1 by ldrop_drop/ #HU2
+lapply (cpr_lift … HV2 (L2.ⓓW2) … HVU2 … HVU) -HVU2 /2 width=2 by ldrop_drop/ #HU2
 elim (cpr_inv_abbr1 … H) -H *
 [ #W1 #T1 #HW01 #HT01 #H destruct
   elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1 by/
@@ -271,8 +271,8 @@ elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1 by/ #V #HV1
 elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1 by/
 elim (IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) /2 width=1 by lpr_pair/ -L0 -V0 -W0 -T0
 elim (lift_total V 0 1) #U #HVU
-lapply (cpr_lift … HV1 (L1.ⓓW1) … HVU1 … HVU) -HVU1 /2 width=1 by ldrop_drop/
-lapply (cpr_lift … HV2 (L2.ⓓW2) … HVU2 … HVU) -HVU2 /2 width=1 by ldrop_drop/
+lapply (cpr_lift … HV1 (L1.ⓓW1) … HVU1 … HVU) -HVU1 /2 width=2 by ldrop_drop/
+lapply (cpr_lift … HV2 (L2.ⓓW2) … HVU2 … HVU) -HVU2 /2 width=2 by ldrop_drop/
 /4 width=7 by cpr_bind, cpr_flat, ex2_intro/ (**) (* full auto not tried *)
 qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma
index 3537c8d01..f9c2374c2 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma
@@ -31,39 +31,41 @@ lemma aaa_cpx_lpx_conf: ∀h,g,G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A →
   elim (cpx_inv_lref1 … H) -H
   [ #H destruct
     elim (lpx_ldrop_conf … HLK1 … HL12) -L1 #X #H #HLK2
-    elim (lpx_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=6/
+    elim (lpx_inv_pair1 … H) -H
+    #K2 #V2 #HK12 #HV12 #H destruct /3 width=6 by aaa_lref/
   | * #J #Y #Z #V2 #H #HV12 #HV2
     lapply (ldrop_mono … H … HLK1) -H #H destruct
     elim (lpx_ldrop_conf … HLK1 … HL12) -L1 #Z #H #HLK2
     elim (lpx_inv_pair1 … H) -H #K2 #V0 #HK12 #_ #H destruct
-    lapply (ldrop_fwd_drop2 … HLK2) -V0 /3 width=7/
+    /3 width=8 by aaa_lift, ldrop_fwd_drop2/
   ]
 | #a #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
   elim (cpx_inv_abbr1 … H) -H *
-  [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=2/
+  [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=2 by lpx_pair, aaa_abbr/
   | #T2 #HT12 #HT2 #H destruct -IHV1
-    @(aaa_inv_lift … (L2.ⓓV1) … HT2) -HT2 /2 width=1/ /3 width=1/
+    /4 width=8 by lpx_pair, aaa_inv_lift, ldrop_drop/
   ]
 | #a #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
-  elim (cpx_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct /4 width=1/
+  elim (cpx_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+  /4 width=1 by lpx_pair, aaa_abst/
 | #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
   elim (cpx_inv_appl1 … H) -H *
-  [ #V2 #T2 #HV12 #HT12 #H destruct /3 width=3/
+  [ #V2 #T2 #HV12 #HT12 #H destruct /3 width=3 by aaa_appl/
   | #b #V2 #W1 #W2 #U1 #U2 #HV12 #HW12 #HU12 #H1 #H2 destruct
     lapply (IHV1 … HV12 … HL12) -IHV1 -HV12 #HV2
-    lapply (IHT1 (ⓛ{b}W2.U2) … HL12) -IHT1 /2 width=1/ -L1 #H
+    lapply (IHT1 (ⓛ{b}W2.U2) … HL12) -IHT1 /2 width=1 by cpx_bind/ -L1 #H
     elim (aaa_inv_abst … H) -H #B0 #A0 #HW1 #HU2 #H destruct
-    lapply (lsuba_aaa_trans … HU2 (L2.ⓓⓝW2.V2) ?) -HU2 /3 width=3/
+    /5 width=6 by lsuba_aaa_trans, lsuba_abbr, aaa_abbr, aaa_cast/
   | #b #V #V2 #W1 #W2 #U1 #U2 #HV1 #HV2 #HW12 #HU12 #H1 #H2 destruct
-    lapply (aaa_lift G L2 … B … (L2.ⓓW2) … HV2) -HV2 /2 width=1/ #HV2
-    lapply (IHT1 (ⓓ{b}W2.U2) … HL12) -IHT1 /2 width=1/ -L1 #H
-    elim (aaa_inv_abbr … H) -H /3 width=3/
+    lapply (aaa_lift G L2 … B … (L2.ⓓW2) … HV2) -HV2 /2 width=2 by ldrop_drop/ #HV2
+    lapply (IHT1 (ⓓ{b}W2.U2) … HL12) -IHT1 /2 width=1 by cpx_bind/ -L1 #H
+    elim (aaa_inv_abbr … H) -H /3 width=3 by aaa_abbr, aaa_appl/
   ]
 | #G #L1 #V1 #T1 #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
   elim (cpx_inv_cast1 … H) -H
-  [ * #V2 #T2 #HV12 #HT12 #H destruct /3 width=1/
-  | -IHV1 /2 width=1/
-  | -IHT1 /2 width=1/
+  [ * #V2 #T2 #HV12 #HT12 #H destruct /3 width=1 by aaa_cast/
+  | -IHV1 /2 width=1 by/
+  | -IHT1 /2 width=1 by/
   ]
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma
index b6c3584ed..188e8d11b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma
@@ -21,10 +21,10 @@ include "basic_2/reduction/lpx.ma".
 (* Properies on local environment slicing ***********************************)
 
 lemma lpx_ldrop_conf: ∀h,g,G. dropable_sn (lpx h g G).
-/3 width=5 by lpx_sn_deliftable_dropable, cpx_inv_lift1/ qed-.
+/3 width=6 by lpx_sn_deliftable_dropable, cpx_inv_lift1/ qed-.
 
 lemma ldrop_lpx_trans: ∀h,g,G. dedropable_sn (lpx h g G).
-/3 width=9 by lpx_sn_liftable_dedropable, cpx_lift/ qed-.
+/3 width=10 by lpx_sn_liftable_dedropable, cpx_lift/ qed-.
 
 lemma lpx_ldrop_trans_O1: ∀h,g,G. dropable_dx (lpx h g G).
 /2 width=3 by lpx_sn_dropable/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma
index 798b6eb79..829fea318 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma
@@ -27,7 +27,7 @@ inductive cpy: ynat → ynat → relation4 genv lenv term term ≝
 | cpy_subst: ∀I,G,L,K,V,W,i,d,e. d ≤ yinj i → i < d+e →
              ⇩[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 V1 V2 → cpy (⫯d) e G (L.ⓑ{I}V1) T1 T2 →
              cpy d e G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
 | cpy_flat : ∀I,G,L,V1,V2,T1,T2,d,e.
              cpy d e G L V1 V2 → cpy d e G L T1 T2 →
@@ -66,7 +66,7 @@ lemma cpy_full: ∀I,G,K,V,T1,L,d. ⇩[d] L ≡ K.ⓑ{I}V →
   /4 width=5 by cpy_subst, ylt_inj, ex2_2_intro/
 | * [ #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
+  [ elim (IHU1 (L.ⓑ{J}W1) (d+1)) -IHU1
     /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/
@@ -145,7 +145,7 @@ lemma cpy_split_up: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶×[d, e] T2 → ∀i.
   elim (IHV12 i) -IHV12 // #V
   elim (IHT12 (i+1)) -IHT12 /2 width=1 by yle_succ/ -Hide
   >yplus_SO2 >yplus_succ1 #T #HT1 #HT2
-  lapply (lsuby_cpy_trans … HT1 (L.ⓑ{I}V) ?) -HT1
+  lapply (lsuby_cpy_trans … HT2 (L.ⓑ{I}V) ?) -HT2
   /3 width=5 by lsuby_succ, ex2_intro, cpy_bind/
 | #I #G #L #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #i #Hide
   elim (IHV12 i) -IHV12 // elim (IHT12 i) -IHT12 // -Hide
@@ -164,7 +164,7 @@ lemma cpy_split_down: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶×[d, e] T2 → ∀
   elim (IHV12 i) -IHV12 // #V
   elim (IHT12 (i+1)) -IHT12 /2 width=1 by yle_succ/ -Hide
   >yplus_SO2 >yplus_succ1 #T #HT1 #HT2
-  lapply (lsuby_cpy_trans … HT1 (L. ⓑ{I} V) ?) -HT1
+  lapply (lsuby_cpy_trans … HT2 (L.ⓑ{I}V) ?) -HT2
   /3 width=5 by lsuby_succ, ex2_intro, cpy_bind/
 | #I #G #L #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #i #Hide
   elim (IHV12 i) -IHV12 // elim (IHT12 i) -IHT12 // -Hide
@@ -230,7 +230,7 @@ qed-.
 fact cpy_inv_bind1_aux: ∀G,L,U1,U2,d,e. ⦃G, L⦄ ⊢ U1 ▶×[d, e] U2 →
                         ∀a,I,V1,T1. U1 = ⓑ{a,I}V1.T1 →
                         ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶×[d, e] V2 &
-                                 ⦃G, L. ⓑ{I}V2⦄ ⊢ T1 ▶×[⫯d, e] T2 &
+                                 ⦃G, L. ⓑ{I}V1⦄ ⊢ T1 ▶×[⫯d, e] T2 &
                                  U2 = ⓑ{a,I}V2.T2.
 #G #L #U1 #U2 #d #e * -G -L -U1 -U2 -d -e
 [ #I #G #L #d #e #b #J #W1 #U1 #H destruct
@@ -242,7 +242,7 @@ qed-.
 
 lemma cpy_inv_bind1: ∀a,I,G,L,V1,T1,U2,d,e. ⦃G, L⦄ ⊢ ⓑ{a,I} V1. T1 ▶×[d, e] U2 →
                      ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶×[d, e] V2 &
-                              ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ▶×[⫯d, e] T2 &
+                              ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶×[⫯d, e] T2 &
                               U2 = ⓑ{a,I}V2.T2.
 /2 width=3 by cpy_inv_bind1_aux/ qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_cpy.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_cpy.ma
index 2acd3705c..a601a989e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_cpy.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_cpy.ma
@@ -32,11 +32,11 @@ theorem cpy_conf_eq: ∀G,L,T0,T1,d1,e1. ⦃G, L⦄ ⊢ T0 ▶×[d1, e1] T1 →
   ]
 | #a #I #G #L #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #X #d2 #e2 #HX
   elim (cpy_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
-  lapply (lsuby_cpy_trans … HT02 (L.ⓑ{I}V1) ?) -HT02 /2 width=1 by lsuby_succ/ #HT02
-  elim (IHV01 … HV02) -V0 #V #HV1 #HV2
+  elim (IHV01 … HV02) -IHV01 -HV02 #V #HV1 #HV2
   elim (IHT01 … HT02) -T0 #T #HT1 #HT2
-  lapply (lsuby_cpy_trans … HT1 (L.ⓑ{I}V) ?) -HT1 /2 width=1 by lsuby_succ/
-  lapply (lsuby_cpy_trans … HT2 (L.ⓑ{I}V) ?) -HT2 /3 width=5 by cpy_bind, lsuby_succ, ex2_intro/
+  lapply (lsuby_cpy_trans … HT1 (L.ⓑ{I}V1) ?) -HT1 /2 width=1 by lsuby_succ/
+  lapply (lsuby_cpy_trans … HT2 (L.ⓑ{I}V2) ?) -HT2
+  /3 width=5 by cpy_bind, lsuby_succ, ex2_intro/
 | #I #G #L #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #X #d2 #e2 #HX
   elim (cpy_inv_flat1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
   elim (IHV01 … HV02) -V0
@@ -60,11 +60,11 @@ theorem cpy_conf_neq: ∀G,L1,T0,T1,d1,e1. ⦃G, L1⦄ ⊢ T0 ▶×[d1, e1] T1 
   ]
 | #a #I #G #L1 #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #L2 #X #d2 #e2 #HX #H
   elim (cpy_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
-  elim (IHV01 … HV02 H) -V0 #V #HV1 #HV2
+  elim (IHV01 … HV02 H) -IHV01 -HV02 #V #HV1 #HV2
   elim (IHT01 … HT02) -T0
   [ -H #T #HT1 #HT2
-    lapply (lsuby_cpy_trans … HT1 (L2.ⓑ{I}V) ?) -HT1 /2 width=1 by lsuby_succ/
-    lapply (lsuby_cpy_trans … HT2 (L1.ⓑ{I}V) ?) -HT2 /3 width=5 by cpy_bind, lsuby_succ, ex2_intro/
+    lapply (lsuby_cpy_trans … HT1 (L2.ⓑ{I}V1) ?) -HT1 /2 width=1 by lsuby_succ/
+    lapply (lsuby_cpy_trans … HT2 (L1.ⓑ{I}V2) ?) -HT2 /3 width=5 by cpy_bind, lsuby_succ, ex2_intro/
   | -HV1 -HV2 elim H -H /3 width=1 by yle_succ, or_introl, or_intror/
   ]
 | #I #G #L1 #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #L2 #X #d2 #e2 #HX #H
@@ -89,9 +89,8 @@ theorem cpy_trans_ge: ∀G,L,T1,T0,d,e. ⦃G, L⦄ ⊢ T1 ▶×[d, e] T0 →
   >yplus_inj #HVT2 <(cpy_inv_lift1_eq … HVW … HVT2) -HVT2 /2 width=5 by cpy_subst/
 | #a #I #G #L #V1 #V0 #T1 #T0 #d #e #_ #_ #IHV10 #IHT10 #X #H #He
   elim (cpy_inv_bind1 … H) -H #V2 #T2 #HV02 #HT02 #H destruct
-  lapply (lsuby_cpy_trans … HT02 (L.ⓑ{I}V0) ?) -HT02 /2 width=1 by lsuby_succ/ #HT02
-  lapply (IHT10 … HT02 He) -T0 #HT12
-  lapply (lsuby_cpy_trans … HT12 (L.ⓑ{I}V2) ?) -HT12 /3 width=1 by cpy_bind, lsuby_succ/
+  lapply (lsuby_cpy_trans … HT02 (L.ⓑ{I}V1) ?) -HT02 /2 width=1 by lsuby_succ/ #HT02
+  lapply (IHT10 … HT02 He) -T0 /3 width=1 by cpy_bind/
 | #I #G #L #V1 #V0 #T1 #T0 #d #e #_ #_ #IHV10 #IHT10 #X #H #He
   elim (cpy_inv_flat1 … H) -H #V2 #T2 #HV02 #HT02 #H destruct /3 width=1 by cpy_flat/
 ]
@@ -108,11 +107,10 @@ theorem cpy_trans_down: ∀G,L,T1,T0,d1,e1. ⦃G, L⦄ ⊢ T1 ▶×[d1, e1] T0 
   >yplus_inj #HWT2 <(cpy_inv_lift1_eq … HVW … HWT2) -HWT2 /3 width=9 by cpy_subst, ex2_intro/
 | #a #I #G #L #V1 #V0 #T1 #T0 #d1 #e1 #_ #_ #IHV10 #IHT10 #X #d2 #e2 #HX #de2d1
   elim (cpy_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
-  lapply (lsuby_cpy_trans … HT02 (L. ⓑ{I} V0) ?) -HT02 /2 width=1 by lsuby_succ/ #HT02
+  lapply (lsuby_cpy_trans … HT02 (L.ⓑ{I}V1) ?) -HT02 /2 width=1 by lsuby_succ/ #HT02
   elim (IHV10 … HV02) -IHV10 -HV02 // #V
   elim (IHT10 … HT02) -T0 /2 width=1 by yle_succ/ #T #HT1 #HT2
-  lapply (lsuby_cpy_trans … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1 by lsuby_succ/
-  lapply (lsuby_cpy_trans … HT2 (L. ⓑ{I} V2) ?) -HT2 /3 width=6 by cpy_bind, lsuby_succ, ex2_intro/
+  lapply (lsuby_cpy_trans … HT2 (L.ⓑ{I}V) ?) -HT2 /3 width=6 by cpy_bind, lsuby_succ, ex2_intro/
 | #I #G #L #V1 #V0 #T1 #T0 #d1 #e1 #_ #_ #IHV10 #IHT10 #X #d2 #e2 #HX #de2d1
   elim (cpy_inv_flat1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
   elim (IHV10 … HV02) -V0 //
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 38ba768e8..8ca9622b9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_lift.ma
@@ -123,7 +123,7 @@ lemma cpy_inv_lift1_le: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 
   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 #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 (IHW12 … HLK … HVW1) -IHW12 // #V2 #HV12 #HVW2
   elim (IHU12 … HTU1) -IHU12 -HTU1
   /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
@@ -162,7 +162,7 @@ lemma cpy_inv_lift1_be: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 
   ]
 | #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 (IHW12 … HLK … HVW1) -IHW12 // #V2 #HV12 #HVW2
   elim (IHU12 … HTU1) -U1
   /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
@@ -198,7 +198,7 @@ lemma cpy_inv_lift1_ge: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 
 | #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 (IHW12 … HLK … HVW1) -IHW12 // #V2 #HV12 #HVW2
   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 #s #d #e #HLK #X #H #Hdetd
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma
index 885bce344..3aae4505c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma
@@ -60,13 +60,11 @@ lemma cpys_refl: ∀G,L,d,e. reflexive … (cpys d e G L).
 /2 width=1 by cpy_cpys/ qed.
 
 lemma cpys_bind: ∀G,L,V1,V2,d,e. ⦃G, L⦄ ⊢ V1 ▶*×[d, e] V2 →
-                 ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ▶*×[⫯d, e] T2 →
+                 ∀I,T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶*×[⫯d, e] T2 →
                  ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*×[d, e] ⓑ{a,I}V2.T2.
 #G #L #V1 #V2 #d #e #HV12 @(cpys_ind … HV12) -V2
 [ #I #T1 #T2 #HT12 @(cpys_ind … HT12) -T2 /3 width=5 by cpys_strap1, cpy_bind/
-| #V #V2 #_ #HV2 #IHV1 #I #T1 #T2 #HT12 #a
-  lapply (lsuby_cpys_trans … HT12 (L.ⓑ{I}V) ?) -HT12
-  /3 width=5 by cpys_strap1, cpy_bind, lsuby_succ/
+| /3 width=5 by cpys_strap1, cpy_bind/
 ]
 qed.
 
@@ -131,13 +129,13 @@ qed-.
 
 lemma cpys_inv_bind1: ∀a,I,G,L,V1,T1,U2,d,e. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*×[d, e] U2 →
                       ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*×[d, e] V2 &
-                               ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ▶*×[⫯d, e] T2 &
+                               ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶*×[⫯d, e] T2 &
                                U2 = ⓑ{a,I}V2.T2.
 #a #I #G #L #V1 #T1 #U2 #d #e #H @(cpys_ind … H) -U2
 [ /2 width=5 by ex3_2_intro/
 | #U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct
   elim (cpy_inv_bind1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H
-  lapply (lsuby_cpys_trans … HT1 (L.ⓑ{I}V2) ?) -HT1
+  lapply (lsuby_cpy_trans … HT2 (L.ⓑ{I}V1) ?) -HT2
   /3 width=5 by cpys_strap1, lsuby_succ, ex3_2_intro/
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma
index 3fb179ed2..746b5c4f4 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma
@@ -24,7 +24,7 @@ inductive cpysa: ynat → ynat → relation4 genv lenv term term ≝
                ⇩[i] L ≡ K.ⓑ{I}V1 → cpysa 0 (⫰(d+e-i)) G K V1 V2 →
                ⇧[0, i+1] V2 ≡ W2 → cpysa d e G L (#i) W2
 | cpysa_bind : ∀a,I,G,L,V1,V2,T1,T2,d,e.
-               cpysa d e G L V1 V2 → cpysa (⫯d) e G (L.ⓑ{I}V2) T1 T2 →
+               cpysa d e G L V1 V2 → cpysa (⫯d) e G (L.ⓑ{I}V1) T1 T2 →
                cpysa d e G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
 | cpysa_flat : ∀I,G,L,V1,V2,T1,T2,d,e.
                cpysa d e G L V1 V2 → cpysa d e G L T1 T2 →
@@ -64,10 +64,7 @@ lemma cpysa_cpy_trans: ∀G,L,T1,T,d,e. ⦃G, L⦄ ⊢ T1 ▶▶*×[d, e] T →
   /3 width=7 by cpysa_subst, ylt_fwd_le_succ/
 | #a #I #G #L #V1 #V #T1 #T #d #e #_ #_ #IHV1 #IHT1 #X #H
   elim (cpy_inv_bind1 … H) -H #V2 #T2 #HV2 #HT2 #H destruct
-  lapply (lsuby_cpy_trans … HT2 (L.ⓑ{I}V) ?) -HT2 /2 width=1 by lsuby_succ/ #HT2
-  lapply (IHV1 … HV2) -IHV1 -HV2 #HV12
-  lapply (IHT1 … HT2) -IHT1 -HT2 #HT12
-  lapply (lsuby_cpysa_trans … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1 by lsuby_succ, cpysa_bind/
+  /5 width=5 by cpysa_bind, lsuby_cpy_trans, lsuby_succ/
 | #I #G #L #V1 #V #T1 #T #d #e #_ #_ #IHV1 #IHT1 #X #H
   elim (cpy_inv_flat1 … H) -H #V2 #T2 #HV2 #HT2 #H destruct /3 width=1 by cpysa_flat/
 ]
@@ -90,8 +87,8 @@ lemma cpys_ind_alt: ∀R:ynat→ynat→relation4 genv lenv term term.
                      ⇧[O, i+1] V2 ≡ W2 → R O (⫰(d+e-i)) G K V1 V2 → R d e G L (#i) W2
                     ) →
                     (∀a,I,G,L,V1,V2,T1,T2,d,e. ⦃G, L⦄ ⊢ V1 ▶*×[d, e] V2 →
-                     ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ▶*×[⫯d, e] T2 → R d e G L V1 V2 →
-                     R (⫯d) e G (L.ⓑ{I}V2) T1 T2 → R d e G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
+                     ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶*×[⫯d, e] T2 → R d e G L V1 V2 →
+                     R (⫯d) e G (L.ⓑ{I}V1) T1 T2 → R d e G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
                     ) →
                     (∀I,G,L,V1,V2,T1,T2,d,e. ⦃G, L⦄ ⊢ V1 ▶*×[d, e] V2 →
                      ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 → R d e G L V1 V2 →
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma
index 47d88486d..d6bef52ec 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma
@@ -50,12 +50,7 @@ lemma lleq_bind: ∀a,I,L1,L2,V,T,d.
 #a #I #L1 #L2 #V #T #d * #HL12 #IHV * #_ #IHT @conj // -HL12
 #X @conj #H elim (cpys_inv_bind1 … H) -H
 #W #U #HVW #HTU #H destruct
-elim (IHV W) -IHV #H1VW #H1WV
-elim (IHT U) -IHT #H1TU #H1UT
-@cpys_bind /2 width=1 by/ -HVW -H1VW -H1WV
-[ @(lsuby_cpys_trans … (L2.ⓑ{I}V))
-| @(lsuby_cpys_trans … (L1.ⓑ{I}V))
-] /4 width=5 by lsuby_cpys_trans, lsuby_succ/ (**) (* full auto too slow *)
+elim (IHV W) -IHV elim (IHT U) -IHT /3 width=1 by cpys_bind/
 qed.
 
 lemma lleq_flat: ∀I,L1,L2,V,T,d.
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 d2d8186af..506fa910b 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
@@ -136,7 +136,7 @@ table {
         ]
         [ { "context-sensitive extended reduction" * } {
              [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_ldrop" + "lpx_lleq" + "lpx_aaa" * ]
-             [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_lift" + "cpx_lleq" + "cpx_cix" * ]
+             [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_lift" + "cpx_cpys" + "cpx_lleq" + "cpx_cix" * ]
           }
         ]
         [ { "context-sensitive extended irreducible forms" * } {
-- 
2.39.2