From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 26 Nov 2011 22:52:35 +0000 (+0000)
Subject: component "reducibility" updated to new syntax!
X-Git-Tag: make_still_working~2056
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=04cd2181640b3828b3d193a8e819c849ef574236;p=helm.git

component "reducibility" updated to new syntax!
---

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr.ma
index 90bd96d4d..3b05c3ea6 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr.ma
@@ -30,13 +30,13 @@ interpretation
 
 (* Basic_1: was by definition: pr2_free *)
 lemma cpr_pr: ∀T1,T2. T1 ⇒ T2 → ∀L. L ⊢ T1 ⇒ T2.
-/2/ qed.
+/2 width=3/ qed.
 
 lemma cpr_tpss: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫* T2 → L ⊢ T1 ⇒ T2.
 /3 width=5/ qed.
 
 lemma cpr_refl: ∀L,T. L ⊢ T ⇒ T.
-/2/ qed.
+/2 width=1/ qed.
 
 (* Note: new property *)
 (* Basic_1: was only: pr2_thin_dx *) 
@@ -47,7 +47,7 @@ qed.
 
 lemma cpr_cast: ∀L,V,T1,T2.
                 L ⊢ T1 ⇒ T2 → L ⊢ 𝕔{Cast} V. T1 ⇒ T2.
-#L #V #T1 #T2 * /3/
+#L #V #T1 #T2 * /3 width=3/
 qed.
 
 (* Note: it does not hold replacing |L1| with |L2| *)
@@ -55,7 +55,7 @@ qed.
 lemma cpr_lsubs_conf: ∀L1,T1,T2. L1 ⊢ T1 ⇒ T2 →
                       ∀L2. L1 [0, |L1|] ≼ L2 → L2 ⊢ T1 ⇒ T2.
 #L1 #T1 #T2 * #T #HT1 #HT2 #L2 #HL12 
-lapply (tpss_lsubs_conf … HT2 … HL12) -HT2 HL12 /3/
+lapply (tpss_lsubs_conf … HT2 … HL12) -HT2 -HL12 /3 width=4/
 qed.
 
 (* Basic inversion lemmas ***************************************************)
@@ -79,9 +79,9 @@ lemma cpr_inv_cast1: ∀L,V1,T1,U2. L ⊢ 𝕔{Cast} V1. T1 ⇒ U2 → (
                                  U2 = 𝕔{Cast} V2. T2
                      ) ∨ L ⊢ T1 ⇒ U2.
 #L #V1 #T1 #U2 * #X #H #HU2
-elim (tpr_inv_cast1 … H) -H /3/
-* #V #T #HV1 #HT1 #H destruct -X;
-elim (tpss_inv_flat1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H destruct -U2 /4 width=5/
+elim (tpr_inv_cast1 … H) -H /3 width=3/
+* #V #T #HV1 #HT1 #H destruct
+elim (tpss_inv_flat1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H destruct /4 width=5/
 qed-.
 
 (* Basic_1: removed theorems 5: 
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_cpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_cpr.ma
index 005e9b0d4..5ac57a614 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_cpr.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_cpr.ma
@@ -22,7 +22,7 @@ include "Basic_2/reducibility/cpr.ma".
 lemma cpr_bind_sn: ∀I,L,V1,V2,T1,T2. L ⊢ V1 ⇒ V2 → T1 ⇒ T2 →
                    L ⊢ 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2.
 #I #L #V1 #V2 #T1 #T2 * #V #HV1 #HV2 #HT12 
-@ex2_1_intro [2: @(tpr_delta … HV1 HT12) | skip ] /2/ (* /3 width=5/ is too slow *)
+@ex2_1_intro [2: @(tpr_delta … HV1 HT12) | skip ] /2 width=3/ (* /3 width=5/ is too slow *)
 qed.
 
 (* Basic_1: was only: pr2_gen_cbind *)
@@ -30,9 +30,9 @@ lemma cpr_bind_dx: ∀I,L,V1,V2,T1,T2. V1 ⇒ V2 → L. 𝕓{I} V2 ⊢ T1 ⇒ T2
                    L ⊢ 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2.
 #I #L #V1 #V2 #T1 #T2 #HV12 * #T #HT1 normalize #HT2
 elim (tpss_split_up … HT2 1 ? ?) -HT2 // #T0 <minus_n_O #HT0 normalize <minus_plus_m_m #HT02
-lapply (tpss_lsubs_conf … HT0 (⋆. 𝕓{I} V2) ?) -HT0 /2/ #HT0
+lapply (tpss_lsubs_conf … HT0 (⋆. 𝕓{I} V2) ?) -HT0 /2 width=1/ #HT0
 lapply (tpss_tps … HT0) -HT0 #HT0
-@ex2_1_intro [2: @(tpr_delta … HV12 HT1 HT0) | skip | /2/ ] (**) (* /3 width=5/ is too slow *)
+@ex2_1_intro [2: @(tpr_delta … HV12 HT1 HT0) | skip | /2 width=1/ ] (**) (* /3 width=5/ is too slow *)
 qed.
 
 (* Advanced forward lemmas **************************************************)
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_lift.ma
index 457cb1b7d..0775cefd2 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_lift.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_lift.ma
@@ -39,14 +39,14 @@ lemma cpr_inv_lref1: ∀L,T2,i. L ⊢ #i ⇒ T2 →
                                 i < |L|.
 #L #T2 #i * #X #H
 >(tpr_inv_atom1 … H) -H #H
-elim (tpss_inv_lref1 … H) -H /2/
+elim (tpss_inv_lref1 … H) -H /2 width=1/
 * /3 width=6/
 qed-.
 
 (* Basic_1: was: pr2_gen_abst *)
 lemma cpr_inv_abst1: ∀V1,T1,U2. 𝕔{Abst} V1. T1 ⇒ U2 →
                      ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Abst} V2. T2.
-/2/ qed-.
+/2 width=3/ qed-.
 
 (* Relocation properties ****************************************************)
 
@@ -58,8 +58,8 @@ lemma cpr_lift: ∀L,K,d,e. ↓[d, e] L ≡ K →
 elim (lift_total T d e) #U #HTU 
 lapply (tpr_lift … HT1 … HTU1 … HTU) -T1 #HU1
 elim (lt_or_ge (|K|) d) #HKd
-[ lapply (tpss_lift_le … HT2 … HLK HTU … HTU2) -T2 T HLK [ /2/ | /3/ ]
-| lapply (tpss_lift_be … HT2 … HLK HTU … HTU2) -T2 T HLK // /3/
+[ lapply (tpss_lift_le … HT2 … HLK HTU … HTU2) -T2 -T -HLK [ /2 width=1/ | /3 width=4/ ]
+| lapply (tpss_lift_be … HT2 … HLK HTU … HTU2) -T2 -T -HLK // /3 width=4/
 ]
 qed.
 
@@ -70,10 +70,10 @@ lemma cpr_inv_lift: ∀L,K,d,e. ↓[d, e] L ≡ K →
 #L #K #d #e #HLK #T1 #U1 #HTU1 #U2 * #U #HU1 #HU2
 elim (tpr_inv_lift … HU1 … HTU1) -U1 #T #HTU #T1
 elim (lt_or_ge (|L|) d) #HLd
-[ elim (tpss_inv_lift1_le … HU2 … HLK … HTU ?) -U HLK [ /5/ | /2/ ]
+[ elim (tpss_inv_lift1_le … HU2 … HLK … HTU ?) -U -HLK [ /5 width=4/ | /2 width=1/ ]
 | elim (lt_or_ge (|L|) (d + e)) #HLde
-  [ elim (tpss_inv_lift1_be_up … HU2 … HLK … HTU ? ?) -U HLK // [ /5/ | /2/ ] 
-  | elim (tpss_inv_lift1_be … HU2 … HLK … HTU ? ?) -U HLK // /5/
+  [ elim (tpss_inv_lift1_be_up … HU2 … HLK … HTU ? ?) -U -HLK // [ /5 width=4/ | /2 width=1/ ] 
+  | elim (tpss_inv_lift1_be … HU2 … HLK … HTU ? ?) -U -HLK // /5 width=4/
   ]
 ]
 qed.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_ltpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_ltpr.ma
index 486c12ee0..1311e5290 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_ltpr.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_ltpr.ma
@@ -25,15 +25,15 @@ lemma cpr_tpss_ltpr: ∀L1,L2. L1 ⇒ L2 → ∀T1,T2. L2 ⊢ T1 ⇒ T2 →
                      ∀d,e,U1. L1 ⊢ T1 [d, e] ≫* U1 →
                      ∃∃U2. L2 ⊢ U1 ⇒ U2 & L2 ⊢ T2 [d, e] ≫* U2.
 #L1 #L2 #HL12 #T1 #T2 * #T #HT1 #HT2 #d #e #U1 #HTU1
-elim (tpr_tpss_ltpr … HL12 … HT1 … HTU1) -L1 HT1 #U #HU1 #HTU
-elim (tpss_conf_eq … HT2 … HTU) -T /3/
+elim (tpr_tpss_ltpr … HL12 … HT1 … HTU1) -L1 -HT1 #U #HU1 #HTU
+elim (tpss_conf_eq … HT2 … HTU) -T /3 width=3/
 qed.
 
 lemma cpr_ltpr_conf_eq: ∀L1,T1,T2. L1 ⊢ T1 ⇒ T2 → ∀L2. L1 ⇒ L2 →
                         ∃∃T. L2 ⊢ T1 ⇒ T & T2 ⇒ T.
 #L1 #T1 #T2 * #T #HT1 #HT2 #L2 #HL12
->(ltpr_fwd_length … HL12) in HT2 #HT2
-elim (tpr_tpss_ltpr … HL12 … HT2) -L1 HT2 /3/
+>(ltpr_fwd_length … HL12) in HT2; #HT2
+elim (tpr_tpss_ltpr … HL12 … HT2) -L1 /3 width=3/
 qed.
 
 lemma cpr_ltpr_conf_tpss: ∀L1,L2. L1 ⇒ L2 → ∀T1,T2. L1 ⊢ T1 ⇒ T2 →
@@ -41,6 +41,6 @@ lemma cpr_ltpr_conf_tpss: ∀L1,L2. L1 ⇒ L2 → ∀T1,T2. L1 ⊢ T1 ⇒ T2 →
                           ∃∃U2. L2 ⊢ U1 ⇒ U2 & L2 ⊢ T2 ⇒ U2.
 #L1 #L2 #HL12 #T1 #T2 #HT12 #d #e #U1 #HTU1
 elim (cpr_ltpr_conf_eq … HT12 … HL12) -HT12 #T #HT1 #HT2
-elim (cpr_tpss_ltpr … HL12 … HT1 … HTU1) -L1 HT1 #U2 #HU12 #HTU2
+elim (cpr_tpss_ltpr … HL12 … HT1 … HTU1) -L1 -HT1 #U2 #HU12 #HTU2
 lapply (tpss_weak_all … HTU2) -HTU2 #HTU2 /3 width=5/ (**) (* /4 width=5/ is too slow *)
 qed.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/lcpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/lcpr.ma
index 13545ad84..30df056e0 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/lcpr.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/lcpr.ma
@@ -28,7 +28,7 @@ interpretation
 (* Basic properties *********************************************************)
 
 lemma lcpr_refl: ∀L. L ⊢ ⇒ L.
-/2/ qed.
+/2 width=3/ qed.
 
 (* Basic inversion lemmas ***************************************************)
 
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr.ma
index b3ba2ff44..2208557a7 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr.ma
@@ -29,13 +29,13 @@ interpretation
 (* Basic properties *********************************************************)
 
 lemma ltpr_refl: ∀L:lenv. L ⇒ L.
-#L elim L -L /2/
+#L elim L -L // /2 width=1/
 qed.
 
 (* Basic inversion lemmas ***************************************************)
 
 fact ltpr_inv_atom1_aux: ∀L1,L2. L1 ⇒ L2 → L1 = ⋆ → L2 = ⋆.
-#L1 #L2 * -L1 L2
+#L1 #L2 * -L1 -L2
 [ //
 | #K1 #K2 #I #V1 #V2 #_ #_ #H destruct
 ]
@@ -43,47 +43,47 @@ qed.
 
 (* Basic_1: was: wcpr0_gen_sort *)
 lemma ltpr_inv_atom1: ∀L2. ⋆ ⇒ L2 → L2 = ⋆.
-/2/ qed-.
+/2 width=3/ qed-.
 
 fact ltpr_inv_pair1_aux: ∀L1,L2. L1 ⇒ L2 → ∀K1,I,V1. L1 = K1. 𝕓{I} V1 →
                          ∃∃K2,V2. K1 ⇒ K2 & V1 ⇒ V2 & L2 = K2. 𝕓{I} V2.
-#L1 #L2 * -L1 L2
+#L1 #L2 * -L1 -L2
 [ #K1 #I #V1 #H destruct
-| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #L #J #W #H destruct - K1 I V1 /2 width=5/
+| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #L #J #W #H destruct /2 width=5/
 ]
 qed.
 
 (* Basic_1: was: wcpr0_gen_head *)
 lemma ltpr_inv_pair1: ∀K1,I,V1,L2. K1. 𝕓{I} V1 ⇒ L2 →
                       ∃∃K2,V2. K1 ⇒ K2 & V1 ⇒ V2 & L2 = K2. 𝕓{I} V2.
-/2/ qed-.
+/2 width=3/ qed-.
 
 fact ltpr_inv_atom2_aux: ∀L1,L2. L1 ⇒ L2 → L2 = ⋆ → L1 = ⋆.
-#L1 #L2 * -L1 L2
+#L1 #L2 * -L1 -L2
 [ //
 | #K1 #K2 #I #V1 #V2 #_ #_ #H destruct
 ]
 qed.
 
 lemma ltpr_inv_atom2: ∀L1. L1 ⇒ ⋆ → L1 = ⋆.
-/2/ qed-.
+/2 width=3/ qed-.
 
 fact ltpr_inv_pair2_aux: ∀L1,L2. L1 ⇒ L2 → ∀K2,I,V2. L2 = K2. 𝕓{I} V2 →
                          ∃∃K1,V1. K1 ⇒ K2 & V1 ⇒ V2 & L1 = K1. 𝕓{I} V1.
-#L1 #L2 * -L1 L2
+#L1 #L2 * -L1 -L2
 [ #K2 #I #V2 #H destruct
-| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #K #J #W #H destruct -K2 I V2 /2 width=5/
+| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #K #J #W #H destruct /2 width=5/
 ]
 qed.
 
 lemma ltpr_inv_pair2: ∀L1,K2,I,V2. L1 ⇒ K2. 𝕓{I} V2 →
                       ∃∃K1,V1. K1 ⇒ K2 & V1 ⇒ V2 & L1 = K1. 𝕓{I} V1.
-/2/ qed-.
+/2 width=3/ qed-.
 
 (* Basic forward lemmas *****************************************************)
 
 lemma ltpr_fwd_length: ∀L1,L2. L1 ⇒ L2 → |L1| = |L2|.
-#L1 #L2 #H elim H -H L1 L2; normalize //
+#L1 #L2 #H elim H -L1 -L2 normalize //
 qed-.
 
 (* Basic_1: removed theorems 2: wcpr0_getl wcpr0_getl_back *)
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_ldrop.ma
index b24c0bad2..38e7858dc 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_ldrop.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_ldrop.ma
@@ -20,33 +20,33 @@ include "Basic_2/reducibility/ltpr.ma".
 (* Basic_1: was: wcpr0_ldrop *)
 lemma ltpr_ldrop_conf: ∀L1,K1,d,e. ↓[d, e] L1 ≡ K1 → ∀L2. L1 ⇒ L2 →
                        ∃∃K2. ↓[d, e] L2 ≡ K2 & K1 ⇒ K2.
-#L1 #K1 #d #e #H elim H -H L1 K1 d e
-[ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2/
+#L1 #K1 #d #e #H elim H -L1 -K1 -d -e
+[ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2 width=3/
 | #K1 #I #V1 #X #H
   elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct /3 width=5/
 | #L1 #K1 #I #V1 #e #_ #IHLK1 #X #H
-  elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct -X;
-  elim (IHLK1 … HL12) -IHLK1 HL12 /3/
+  elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
+  elim (IHLK1 … HL12) -L1 /3 width=3/
 | #L1 #K1 #I #V1 #W1 #d #e #_ #HWV1 #IHLK1 #X #H
-  elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct -X;
-  elim (tpr_inv_lift … HV12 … HWV1) -HV12 HWV1;
-  elim (IHLK1 … HL12) -IHLK1 HL12 /3 width=5/
+  elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
+  elim (tpr_inv_lift … HV12 … HWV1) -V1
+  elim (IHLK1 … HL12) -L1 /3 width=5/
 ]
 qed.
 
 (* Basic_1: was: wcpr0_ldrop_back *)
 lemma ltpr_ldrop_trans: ∀L1,K1,d,e. ↓[d, e] L1 ≡ K1 → ∀K2. K1 ⇒ K2 →
                         ∃∃L2. ↓[d, e] L2 ≡ K2 & L1 ⇒ L2.
-#L1 #K1 #d #e #H elim H -H L1 K1 d e
-[ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2/
+#L1 #K1 #d #e #H elim H -L1 -K1 -d -e
+[ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2 width=3/
 | #K1 #I #V1 #X #H
   elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=5/
 | #L1 #K1 #I #V1 #e #_ #IHLK1 #K2 #HK12
-  elim (IHLK1 … HK12) -IHLK1 HK12 /3 width=5/
+  elim (IHLK1 … HK12) -K1 /3 width=5/
 | #L1 #K1 #I #V1 #W1 #d #e #_ #HWV1 #IHLK1 #X #H
-  elim (ltpr_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct -X;
+  elim (ltpr_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct
   elim (lift_total W2 d e) #V2 #HWV2
-  lapply (tpr_lift … HW12 … HWV1 … HWV2) -HW12 HWV1;
-  elim (IHLK1 … HK12) -IHLK1 HK12 /3 width=5/
+  lapply (tpr_lift … HW12 … HWV1 … HWV2) -W1
+  elim (IHLK1 … HK12) -K1 /3 width=5/
 ]
 qed.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf.ma
index 5772e7626..1353c7f06 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf.ma
@@ -28,30 +28,30 @@ interpretation
 
 lemma tnf_inv_abst: ∀V,T. ℕ[𝕔{Abst}V.T] → ℕ[V] ∧ ℕ[T].
 #V1 #T1 #HVT1 @conj
-[ #V2 #HV2 lapply (HVT1 (𝕔{Abst}V2.T1) ?) -HVT1 /2/ -HV2 #H destruct -V1 T1 //
-| #T2 #HT2 lapply (HVT1 (𝕔{Abst}V1.T2) ?) -HVT1 /2/ -HT2 #H destruct -V1 T1 //
+[ #V2 #HV2 lapply (HVT1 (𝕔{Abst}V2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (𝕔{Abst}V1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct //
 ]
 qed-.
 
 lemma tnf_inv_appl: ∀V,T. ℕ[𝕔{Appl}V.T] → ∧∧ ℕ[V] & ℕ[T] & 𝕊[T].
 #V1 #T1 #HVT1 @and3_intro
-[ #V2 #HV2 lapply (HVT1 (𝕔{Appl}V2.T1) ?) -HVT1 /2/ -HV2 #H destruct -V1 T1 //
-| #T2 #HT2 lapply (HVT1 (𝕔{Appl}V1.T2) ?) -HVT1 /2/ -HT2 #H destruct -V1 T1 //
-| generalize in match HVT1 -HVT1; elim T1 -T1 * // * #W1 #U1 #_ #_ #H
+[ #V2 #HV2 lapply (HVT1 (𝕔{Appl}V2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (𝕔{Appl}V1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct //
+| generalize in match HVT1; -HVT1 elim T1 -T1 * // * #W1 #U1 #_ #_ #H
   [ elim (lift_total V1 0 1) #V2 #HV12
-    lapply (H (𝕔{Abbr}W1.𝕔{Appl}V2.U1) ?) -H /2/ -HV12 #H destruct
-  | lapply (H (𝕔{Abbr}V1.U1) ?) -H /2/ #H destruct
+    lapply (H (𝕔{Abbr}W1.𝕔{Appl}V2.U1) ?) -H /2 width=3/ -HV12 #H destruct
+  | lapply (H (𝕔{Abbr}V1.U1) ?) -H /2 width=1/ #H destruct
 ]
 qed-.
 
 lemma tnf_inv_abbr: ∀V,T. ℕ[𝕔{Abbr}V.T] → False.
 #V #T #H elim (is_lift_dec T 0 1)
 [ * #U #HTU
-  lapply (H U ?) -H /2 width=3/ #H destruct -U;
+  lapply (H U ?) -H /2 width=3/ #H destruct
   elim (lift_inv_pair_xy_y … HTU)
 | #HT
   elim (tps_full (⋆) V T (⋆. 𝕓{Abbr} V) 0 ?) // #T2 #T1 #HT2 #HT12
-  lapply (H (𝕓{Abbr}V.T2) ?) -H /2/ -HT2 #H destruct -T /3 width=2/
+  lapply (H (𝕓{Abbr}V.T2) ?) -H /2 width=3/ -HT2 #H destruct /3 width=2/
 ]
 qed.
 
@@ -63,7 +63,7 @@ qed-.
 (* Basic properties *********************************************************)
 
 lemma tpr_tif_eq: ∀T1,T2. T1 ⇒ T2 →  𝕀[T1] → T1 = T2.
-#T1 #T2 #H elim H -T1 T2
+#T1 #T2 #H elim H -T1 -T2
 [ //
 | * #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H
   [ elim (tif_inv_appl … H) -H #HV1 #HT1 #_
@@ -74,7 +74,7 @@ lemma tpr_tif_eq: ∀T1,T2. T1 ⇒ T2 →  𝕀[T1] → T1 = T2.
   elim (tif_inv_appl … H) -H #_ #_ #H
   elim (simple_inv_bind … H)
 | * #V1 #V2 #T1 #T #T2 #_ #_ #HT2 #IHV1 #IHT1 #H
-  [ -HT2 IHV1 IHT1; elim (tif_inv_abbr … H)
+  [ -HT2 -IHV1 -IHT1 elim (tif_inv_abbr … H)
   | <(tps_inv_refl_SO2 … HT2 ?) -HT2 //
     elim (tif_inv_abst … H) -H #HV1 #HT1
     >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 //
@@ -90,15 +90,15 @@ lemma tpr_tif_eq: ∀T1,T2. T1 ⇒ T2 →  𝕀[T1] → T1 = T2.
 qed.
 
 theorem tif_tnf: ∀T1.  𝕀[T1] → ℕ[T1].
-/2/ qed.
+/2 width=1/ qed.
 
 (* Note: this property is unusual *)
 theorem tnf_trf_false: ∀T1. ℝ[T1] → ℕ[T1] → False.
 #T1 #H elim H -T1
-[ #V #T #_ #IHV #H elim (tnf_inv_abst … H) -H /2/
-| #V #T #_ #IHT #H elim (tnf_inv_abst … H) -H /2/
-| #V #T #_ #IHV #H elim (tnf_inv_appl … H) -H /2/
-| #V #T #_ #IHV #H elim (tnf_inv_appl … H) -H /2/
+[ #V #T #_ #IHV #H elim (tnf_inv_abst … H) -H /2 width=1/
+| #V #T #_ #IHT #H elim (tnf_inv_abst … H) -H /2 width=1/
+| #V #T #_ #IHV #H elim (tnf_inv_appl … H) -H /2 width=1/
+| #V #T #_ #IHV #H elim (tnf_inv_appl … H) -H /2 width=1/
 | #V #T #H elim (tnf_inv_abbr … H)
 | #V #T #H elim (tnf_inv_cast … H)
 | #V #W #T #H elim (tnf_inv_appl … H) -H #_ #_ #H
@@ -107,7 +107,7 @@ theorem tnf_trf_false: ∀T1. ℝ[T1] → ℕ[T1] → False.
 qed.
 
 theorem tnf_tif: ∀T1. ℕ[T1] → 𝕀[T1].
-/2/ qed.
+/2 width=3/ qed.
 
 lemma tnf_abst: ∀V,T. ℕ[V] → ℕ[T] → ℕ[𝕔{Abst}V.T].
 /4 width=1/ qed.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr.ma
index f2818ea72..cf0c7cae2 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr.ma
@@ -44,18 +44,18 @@ interpretation
 
 lemma tpr_bind: ∀I,V1,V2,T1,T2. V1 ⇒ V2 → T1 ⇒ T2 →
                                 𝕓{I} V1. T1 ⇒  𝕓{I} V2. T2.
-/2/ qed.
+/2 width=3/ qed.
 
 (* Basic_1: was by definition: pr0_refl *)
 lemma tpr_refl: ∀T. T ⇒ T.
 #T elim T -T //
-#I elim I -I /2/
+#I elim I -I /2 width=1/
 qed.
 
 (* Basic inversion lemmas ***************************************************)
 
 fact tpr_inv_atom1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I. U1 = 𝕒{I} → U2 = 𝕒{I}.
-#U1 #U2 * -U1 U2
+#U1 #U2 * -U1 -U2
 [ //
 | #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct
 | #V1 #V2 #W #T1 #T2 #_ #_ #k #H destruct
@@ -68,7 +68,7 @@ qed.
 
 (* Basic_1: was: pr0_gen_sort pr0_gen_lref *)
 lemma tpr_inv_atom1: ∀I,U2. 𝕒{I} ⇒ U2 → U2 = 𝕒{I}.
-/2/ qed-.
+/2 width=3/ qed-.
 
 fact tpr_inv_bind1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I,V1,T1. U1 = 𝕓{I} V1. T1 →
                         (∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
@@ -76,13 +76,13 @@ fact tpr_inv_bind1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I,V1,T1. U1 = 𝕓{I} V1. T1
                                     U2 = 𝕓{I} V2. T
                         ) ∨
                         ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr.
-#U1 #U2 * -U1 U2
+#U1 #U2 * -U1 -U2
 [ #J #I #V #T #H destruct
 | #I1 #V1 #V2 #T1 #T2 #_ #_ #I #V #T #H destruct
 | #V1 #V2 #W #T1 #T2 #_ #_ #I #V #T #H destruct
-| #I1 #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #I0 #V0 #T0 #H destruct -I1 V1 T1 /3 width=7/
+| #I1 #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #I0 #V0 #T0 #H destruct /3 width=7/
 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #I0 #V0 #T0 #H destruct
-| #V #T #T1 #T2 #HT1 #HT12 #I0 #V0 #T0 #H destruct -V T /3/
+| #V #T #T1 #T2 #HT1 #HT12 #I0 #V0 #T0 #H destruct /3 width=3/
 | #V #T1 #T2 #_ #I0 #V0 #T0 #H destruct
 ]
 qed.
@@ -93,7 +93,7 @@ lemma tpr_inv_bind1: ∀V1,T1,U2,I. 𝕓{I} V1. T1 ⇒ U2 →
                                  U2 = 𝕓{I} V2. T
                      ) ∨
                      ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr.
-/2/ qed-.
+/2 width=3/ qed-.
 
 (* Basic_1: was pr0_gen_abbr *)
 lemma tpr_inv_abbr1: ∀V1,T1,U2. 𝕓{Abbr} V1. T1 ⇒ U2 →
@@ -118,15 +118,14 @@ fact tpr_inv_flat1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I,V1,U0. U1 = 𝕗{I} V1. U0
                                                U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2 &
                                                I = Appl
                          |                     (U0 ⇒ U2 ∧ I = Cast).
-#U1 #U2 * -U1 U2
+#U1 #U2 * -U1 -U2
 [ #I #J #V #T #H destruct
-| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #J #V #T #H destruct -I V1 T1 /3 width=5/
-| #V1 #V2 #W #T1 #T2 #HV12 #HT12 #J #V #T #H destruct -J V1 T /3 width=8/
+| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #J #V #T #H destruct /3 width=5/
+| #V1 #V2 #W #T1 #T2 #HV12 #HT12 #J #V #T #H destruct /3 width=8/
 | #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #J #V0 #T0 #H destruct
-| #V #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #J #V0 #T0 #H
-  destruct -J V1 T0 /3 width=12/
+| #V #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #J #V0 #T0 #H destruct /3 width=12/
 | #V #T #T1 #T2 #_ #_ #J #V0 #T0 #H destruct
-| #V #T1 #T2 #HT12 #J #V0 #T0 #H destruct -J V T1 /3/
+| #V #T1 #T2 #HT12 #J #V0 #T0 #H destruct /3 width=1/
 ]
 qed.
 
@@ -142,7 +141,7 @@ lemma tpr_inv_flat1: ∀V1,U0,U2,I. 𝕗{I} V1. U0 ⇒ U2 →
                                             U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2 &
                                             I = Appl
                       |                     (U0 ⇒ U2 ∧ I = Cast).
-/2/ qed-.
+/2 width=3/ qed-.
 
 (* Basic_1: was pr0_gen_appl *)
 lemma tpr_inv_appl1: ∀V1,U0,U2. 𝕔{Appl} V1. U0 ⇒ U2 →
@@ -166,9 +165,9 @@ lemma tpr_inv_appl1_simple: ∀V1,T1,U. 𝕔{Appl} V1. T1 ⇒ U → 𝕊[T1] →
 #V1 #T1 #U #H #HT1
 elim (tpr_inv_appl1 … H) -H *
 [ /2 width=5/
-| #V2 #W #W1 #W2 #_ #_ #H #_ destruct -T1;
+| #V2 #W #W1 #W2 #_ #_ #H #_ destruct
   elim (simple_inv_bind … HT1)
-| #V2 #V #W1 #W2 #U1 #U2 #_ #_ #_ #_ #H #_ destruct -T1;
+| #V2 #V #W1 #W2 #U1 #U2 #_ #_ #_ #_ #H #_ destruct
   elim (simple_inv_bind … HT1)
 ]
 qed-.
@@ -189,14 +188,14 @@ fact tpr_inv_lref2_aux: ∀T1,T2. T1 ⇒ T2 → ∀i. T2 = #i →
                          | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i &
                                      T1 = 𝕔{Abbr} V. T
                          | ∃∃V,T.    T ⇒ #i & T1 = 𝕔{Cast} V. T.
-#T1 #T2 * -T1 T2
-[ #I #i #H destruct /2/
+#T1 #T2 * -T1 -T2
+[ #I #i #H destruct /2 width=1/
 | #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
 | #V1 #V2 #W #T1 #T2 #_ #_ #i #H destruct
 | #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #i #H destruct
 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
 | #V #T #T1 #T2 #HT1 #HT12 #i #H destruct /3 width=6/
-| #V #T1 #T2 #HT12 #i #H destruct /3/
+| #V #T1 #T2 #HT12 #i #H destruct /3 width=4/
 ]
 qed.
 
@@ -205,7 +204,7 @@ lemma tpr_inv_lref2: ∀T1,i. T1 ⇒ #i →
                       | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i &
                                   T1 = 𝕔{Abbr} V. T
                       | ∃∃V,T.    T ⇒ #i & T1 = 𝕔{Cast} V. T.
-/2/ qed-.
+/2 width=3/ qed-.
 
 (* Basic_1: removed theorems 3:
             pr0_subst0_back pr0_subst0_fwd pr0_subst0
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma
index a30dcddac..d9d9c549a 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma
@@ -22,37 +22,37 @@ include "Basic_2/reducibility/tpr.ma".
 (* Basic_1: was: pr0_lift *)
 lemma tpr_lift: ∀T1,T2. T1 ⇒ T2 →
                 ∀d,e,U1. ↑[d, e] T1 ≡ U1 → ∀U2. ↑[d, e] T2 ≡ U2 → U1 ⇒ U2.
-#T1 #T2 #H elim H -H T1 T2
+#T1 #T2 #H elim H -T1 -T2
 [ * #i #d #e #U1 #HU1 #U2 #HU2
-  lapply (lift_mono … HU1 … HU2) -HU1 #H destruct -U1
-  [ lapply (lift_inv_sort1 … HU2) -HU2 #H destruct -U2 //
-  | lapply (lift_inv_lref1 … HU2) * * #Hid #H destruct -U2 //
-  | lapply (lift_inv_gref1 … HU2) -HU2 #H destruct -U2 //
+  lapply (lift_mono … HU1 … HU2) -HU1 #H destruct
+  [ lapply (lift_inv_sort1 … HU2) -HU2 #H destruct //
+  | lapply (lift_inv_lref1 … HU2) * * #Hid #H destruct //
+  | lapply (lift_inv_gref1 … HU2) -HU2 #H destruct //
   ]
 | #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2
-  elim (lift_inv_flat1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1;
-  elim (lift_inv_flat1 … HX2) -HX2 #W2 #U2 #HVW2 #HTU2 #HX2 destruct -X2 /3/
+  elim (lift_inv_flat1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct
+  elim (lift_inv_flat1 … HX2) -HX2 #W2 #U2 #HVW2 #HTU2 #HX2 destruct /3 width=4/
 | #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2
-  elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct -X1;
-  elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct -X;
-  elim (lift_inv_bind1 … HX2) -HX2 #V3 #T3 #HV23 #HT23 #HX2 destruct -X2 /3/
+  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 #V3 #T3 #HV23 #HT23 #HX2 destruct /3 width=4/
 | #I #V1 #V2 #T1 #T2 #T0 #HV12 #HT12 #HT2 #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2
-  elim (lift_inv_bind1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1;
-  elim (lift_inv_bind1 … HX2) -HX2 #W2 #U0 #HVW2 #HTU0 #HX2 destruct -X2;
+  elim (lift_inv_bind1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct
+  elim (lift_inv_bind1 … HX2) -HX2 #W2 #U0 #HVW2 #HTU0 #HX2 destruct
   elim (lift_total T2 (d + 1) e) #U2 #HTU2
   @tpr_delta
-  [4: @(tps_lift_le … HT2 … HTU2 HTU0 ?) /2/ |1: skip |2: /2/ |3: /2/ ] (**) (*/3. is too slow *)
+  [4: @(tps_lift_le … HT2 … HTU2 HTU0 ?) /2 width=1/ |1: skip |2: /2 width=4/ |3: /2 width=4/ ] (**) (*/3. is too slow *)
 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #X1 #HX1 #X2 #HX2
-  elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct -X1;
-  elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct -X;
-  elim (lift_inv_bind1 … HX2) -HX2 #W3 #X #HW23 #HX #HX2 destruct -X2;
-  elim (lift_inv_flat1 … HX) -HX #V3 #T3 #HV3 #HT23 #HX destruct -X;
-  elim (lift_trans_ge … HV2 … HV3 ?) -HV2 HV3 V // /3/
+  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 ?) -V // /3 width=4/
 | #V #T #T1 #T2 #HT1 #_ #IHT12 #d #e #X #HX #T0 #HT20
-  elim (lift_inv_bind1 … HX) -HX #V3 #T3 #_ #HT3 #HX destruct -X;
-  elim (lift_trans_ge … HT1 … HT3 ?) -HT1 HT3 T // /3 width=6/
+  elim (lift_inv_bind1 … HX) -HX #V3 #T3 #_ #HT3 #HX destruct
+  elim (lift_trans_ge … HT1 … HT3 ?) -T // /3 width=6/
 | #V #T1 #T2 #_ #IHT12 #d #e #X #HX #T #HT2
-  elim (lift_inv_flat1 … HX) -HX #V0 #T0 #_ #HT0 #HX destruct -X /3/
+  elim (lift_inv_flat1 … HX) -HX #V0 #T0 #_ #HT0 #HX destruct /3 width=4/
 ]
 qed.
 
@@ -60,42 +60,42 @@ qed.
 lemma tpr_inv_lift: ∀T1,T2. T1 ⇒ T2 →
                     ∀d,e,U1. ↑[d, e] U1 ≡ T1 →
                     ∃∃U2. ↑[d, e] U2 ≡ T2 & U1 ⇒ U2.
-#T1 #T2 #H elim H -H T1 T2
+#T1 #T2 #H elim H -T1 -T2
 [ * #i #d #e #U1 #HU1
-  [ lapply (lift_inv_sort2 … HU1) -HU1 #H destruct -U1 /2/
-  | lapply (lift_inv_lref2 … HU1) -HU1 * * #Hid #H destruct -U1 /3/
-  | lapply (lift_inv_gref2 … HU1) -HU1 #H destruct -U1 /2/
+  [ lapply (lift_inv_sort2 … HU1) -HU1 #H destruct /2 width=3/
+  | lapply (lift_inv_lref2 … HU1) -HU1 * * #Hid #H destruct /3 width=3/
+  | lapply (lift_inv_gref2 … HU1) -HU1 #H destruct /2 width=3/
   ]
 | #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X #HX
-  elim (lift_inv_flat2 … HX) -HX #V0 #T0 #HV01 #HT01 #HX destruct -X;
-  elim (IHV12 … HV01) -IHV12 HV01;
-  elim (IHT12 … HT01) -IHT12 HT01 /3 width=5/
+  elim (lift_inv_flat2 … HX) -HX #V0 #T0 #HV01 #HT01 #HX destruct
+  elim (IHV12 … HV01) -V1
+  elim (IHT12 … HT01) -T1 /3 width=5/
 | #V1 #V2 #W1 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X #HX
-  elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct -X;
-  elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct -Y;
-  elim (IHV12 … HV01) -IHV12 HV01;
-  elim (IHT12 … HT01) -IHT12 HT01 /3 width=5/
+  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 … HV01) -V1
+  elim (IHT12 … HT01) -T1 /3 width=5/
 | #I #V1 #V2 #T1 #T2 #T0 #_ #_ #HT20 #IHV12 #IHT12 #d #e #X #HX
-  elim (lift_inv_bind2 … HX) -HX #W1 #U1 #HWV1 #HUT1 #HX destruct -X;
-  elim (IHV12 … HWV1) -IHV12 HWV1 #W2 #HWV2 #HW12
-  elim (IHT12 … HUT1) -IHT12 HUT1 #U2 #HUT2 #HU12
-  elim (tps_inv_lift1_le … HT20 … HUT2 ?) -HT20 HUT2 // [3: /2 width=5/ |2: skip ] #U0 #HU20 #HUT0
-  @ex2_1_intro  [2: /2/ |1: skip |3: /2/ ] (**) (* /3 width=5/ is slow *)
+  elim (lift_inv_bind2 … HX) -HX #W1 #U1 #HWV1 #HUT1 #HX destruct
+  elim (IHV12 … HWV1) -V1 #W2 #HWV2 #HW12
+  elim (IHT12 … HUT1) -T1 #U2 #HUT2 #HU12
+  elim (tps_inv_lift1_le … HT20 … HUT2 ?) -T2 // [3: /2 width=5/ |2: skip ] #U0 #HU20 #HUT0
+  @ex2_1_intro  [2: /2 width=2/ |1: skip |3: /2 width=3/ ] (**) (* /3 width=5/ is slow *)
 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #X #HX
-  elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct -X;
-  elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct -Y;
-  elim (IHV12 … HV01) -IHV12 HV01 #V3 #HV32 #HV03
-  elim (IHW12 … HW01) -IHW12 HW01 #W3 #HW32 #HW03
-  elim (IHT12 … HT01) -IHT12 HT01 #T3 #HT32 #HT03
-  elim (lift_trans_le … HV32 … HV2 ?) -HV32 HV2 V2 // #V2 #HV32 #HV2
-  @ex2_1_intro [2: /3/ |1: skip |3: /2/ ] (**) (* /4 width=5/ is slow *)
+  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 … HV01) -V1 #V3 #HV32 #HV03
+  elim (IHW12 … HW01) -W1 #W3 #HW32 #HW03
+  elim (IHT12 … HT01) -T1 #T3 #HT32 #HT03
+  elim (lift_trans_le … HV32 … HV2 ?) -V2 // #V2 #HV32 #HV2
+  @ex2_1_intro [2: /3 width=2/ |1: skip |3: /2 width=3/ ] (**) (* /4 width=5/ is slow *)
 | #V #T #T1 #T2 #HT1 #_ #IHT12 #d #e #X #HX
-  elim (lift_inv_bind2 … HX) -HX #V0 #T0 #_ #HT0 #H destruct -X;
-  elim (lift_div_le … HT1 … HT0 ?) -HT1 HT0 T // #T #HT0 #HT1
-  elim (IHT12 … HT1) -IHT12 HT1 /3 width=5/
+  elim (lift_inv_bind2 … HX) -HX #V0 #T0 #_ #HT0 #H destruct
+  elim (lift_div_le … HT1 … HT0 ?) -T // #T #HT0 #HT1
+  elim (IHT12 … HT1) -T1 /3 width=5/
 | #V #T1 #T2 #_ #IHT12 #d #e #X #HX
-  elim (lift_inv_flat2 … HX) -HX #V0 #T0 #_ #HT01 #H destruct -X;
-  elim (IHT12 … HT01) -IHT12 HT01 /3/
+  elim (lift_inv_flat2 … HX) -HX #V0 #T0 #_ #HT01 #H destruct
+  elim (IHT12 … HT01) -T1 /3 width=3/
 ]
 qed.
 
@@ -103,12 +103,12 @@ qed.
 
 fact tpr_inv_abst1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕔{Abst} V1. T1 →
                         ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Abst} V2. T2.
-#U1 #U2 * -U1 U2
+#U1 #U2 * -U1 -U2
 [ #I #V #T #H destruct
 | #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
 | #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct
-| #I #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #V0 #T0 #H destruct -I V1 T1;
-  <(tps_inv_refl_SO2 … HT2 ? ? ?) -HT2 T /2 width=5/
+| #I #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #V0 #T0 #H destruct
+  <(tps_inv_refl_SO2 … HT2 ? ? ?) -T /2 width=5/
 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct
 | #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct
 | #V #T1 #T2 #_ #V0 #T0 #H destruct
@@ -118,4 +118,4 @@ qed.
 (* Basic_1: was pr0_gen_abst *)
 lemma tpr_inv_abst1: ∀V1,T1,U2. 𝕔{Abst} V1. T1 ⇒ U2 →
                      ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Abst} V2. T2.
-/2/ qed-.
+/2 width=3/ qed-.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpr.ma
index 4217ced9a..332575c21 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpr.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpr.ma
@@ -19,7 +19,7 @@ include "Basic_2/reducibility/tpr_tpss.ma".
 (* Confluence lemmas ********************************************************)
 
 fact tpr_conf_atom_atom: ∀I. ∃∃X. 𝕒{I} ⇒ X & 𝕒{I} ⇒ X.
-/2/ qed.
+/2 width=3/ qed.
 
 fact tpr_conf_flat_flat:
    ∀I,V0,V1,T0,T1,V2,T2. (
@@ -30,8 +30,8 @@ fact tpr_conf_flat_flat:
    V0 ⇒ V1 → V0 ⇒ V2 → T0 ⇒ T1 → T0 ⇒ T2 →
    ∃∃T0. 𝕗{I} V1. T1 ⇒ T0 & 𝕗{I} V2. T2 ⇒ T0.
 #I #V0 #V1 #T0 #T1 #V2 #T2 #IH #HV01 #HV02 #HT01 #HT02
-elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2
-elim (IH … HT01 … HT02) -HT01 HT02 /3 width=5/
+elim (IH … HV01 … HV02) -HV01 -HV02 // #V #HV1 #HV2
+elim (IH … HT01 … HT02) -HT01 -HT02 -IH // /3 width=5/
 qed.
 
 fact tpr_conf_flat_beta:
@@ -44,9 +44,9 @@ fact tpr_conf_flat_beta:
    U0 ⇒ T2 → 𝕔{Abst} W0. U0 ⇒ T1 →
    ∃∃X. 𝕔{Appl} V1. T1 ⇒ X & 𝕔{Abbr} V2. T2 ⇒ X.
 #V0 #V1 #T1 #V2 #W0 #U0 #T2 #IH #HV01 #HV02 #HT02 #H
-elim (tpr_inv_abst1 … H) -H #W1 #U1 #HW01 #HU01 #H destruct -T1;
-elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2
-elim (IH … HT02 … HU01) -HT02 HU01 IH /3 width=5/
+elim (tpr_inv_abst1 … H) -H #W1 #U1 #HW01 #HU01 #H destruct
+elim (IH … HV01 … HV02) -HV01 -HV02 // #V #HV1 #HV2
+elim (IH … HT02 … HU01) -HT02 -HU01 -IH // /3 width=5/
 qed.
 
 (* basic-1: was:
@@ -63,25 +63,25 @@ fact tpr_conf_flat_theta:
    W0 ⇒ W2 → U0 ⇒ U2 →  𝕔{Abbr} W0. U0 ⇒ T1 →
    ∃∃X. 𝕔{Appl} V1. T1 ⇒ X & 𝕔{Abbr} W2. 𝕔{Appl} V. U2 ⇒ X.
 #V0 #V1 #T1 #V2 #V #W0 #W2 #U0 #U2 #IH #HV01 #HV02 #HV2 #HW02 #HU02 #H
-elim (IH … HV01 … HV02) -HV01 HV02 // #VV #HVV1 #HVV2
+elim (IH … HV01 … HV02) -HV01 -HV02 // #VV #HVV1 #HVV2
 elim (lift_total VV 0 1) #VVV #HVV
 lapply (tpr_lift … HVV2 … HV2 … HVV) #HVVV
 elim (tpr_inv_abbr1 … H) -H *
 (* case 1: delta *)
-[ -HV2 HVV2 #WW2 #UU2 #UU #HWW2 #HUU02 #HUU2 #H destruct -T1;
-  elim (IH … HW02 … HWW2) -HW02 HWW2 // #W #HW02 #HWW2
-  elim (IH … HU02 … HUU02) -HU02 HUU02 IH // #U #HU2 #HUUU2
-  elim (tpr_tps_bind … HWW2 HUUU2 … HUU2) -HUU2 HUUU2 #UUU #HUUU2 #HUUU1
+[ -HV2 -HVV2 #WW2 #UU2 #UU #HWW2 #HUU02 #HUU2 #H destruct
+  elim (IH … HW02 … HWW2) -HW02 -HWW2 // #W #HW02 #HWW2
+  elim (IH … HU02 … HUU02) -HU02 -HUU02 -IH // #U #HU2 #HUUU2
+  elim (tpr_tps_bind … HWW2 HUUU2 … HUU2) -UU2 #UUU #HUUU2 #HUUU1
   @ex2_1_intro
   [2: @tpr_theta [6: @HVV |7: @HWW2 |8: @HUUU2 |1,2,3,4: skip | // ]
   |1:skip
   |3: @tpr_delta [3: @tpr_flat |1: skip ] /2 width=5/
   ] (**) (* /5 width=14/ is too slow *)
 (* case 3: zeta *)
-| -HW02 HVV HVVV #UU1 #HUU10 #HUUT1
+| -HW02 -HVV -HVVV #UU1 #HUU10 #HUUT1
   elim (tpr_inv_lift … HU02 … HUU10) -HU02 #UU #HUU2 #HUU1
   lapply (tw_lift … HUU10) -HUU10 #HUU10
-  elim (IH … HUUT1 … HUU1) -HUUT1 HUU1 IH // -HUU10 #U #HU2 #HUUU2
+  elim (IH … HUUT1 … HUU1) -HUUT1 -HUU1 -IH // -HUU10 #U #HU2 #HUUU2
   @ex2_1_intro
   [2: @tpr_flat
   |1: skip 
@@ -99,7 +99,7 @@ fact tpr_conf_flat_cast:
    V0 ⇒ V1 → T0 ⇒ T1 → T0 ⇒ X2 →
    ∃∃X. 𝕔{Cast} V1. T1 ⇒ X & X2 ⇒ X.
 #X2 #V0 #V1 #T0 #T1 #IH #_ #HT01 #HT02
-elim (IH … HT01 … HT02) -HT01 HT02 IH /3/
+elim (IH … HT01 … HT02) -HT01 -HT02 -IH // /3 width=3/
 qed.
 
 fact tpr_conf_beta_beta:
@@ -111,8 +111,8 @@ fact tpr_conf_beta_beta:
    V0 ⇒ V1 → V0 ⇒ V2 → T0 ⇒ T1 → T0 ⇒ T2 →
    ∃∃X. 𝕔{Abbr} V1. T1 ⇒X & 𝕔{Abbr} V2. T2 ⇒ X.
 #W0 #V0 #V1 #T0 #T1 #V2 #T2 #IH #HV01 #HV02 #HT01 #HT02
-elim (IH … HV01 … HV02) -HV01 HV02 //
-elim (IH … HT01 … HT02) -HT01 HT02 IH /3 width=5/
+elim (IH … HV01 … HV02) -HV01 -HV02 //
+elim (IH … HT01 … HT02) -HT01 -HT02 -IH // /3 width=5/
 qed.
 
 (* Basic_1: was: pr0_cong_delta pr0_delta_delta *)
@@ -127,11 +127,11 @@ fact tpr_conf_delta_delta:
    ⋆. 𝕓{I1} V2 ⊢ T2 [O, 1] ≫ TT2 →
    ∃∃X. 𝕓{I1} V1. TT1 ⇒ X & 𝕓{I1} V2. TT2 ⇒ X.
 #I1 #V0 #V1 #T0 #T1 #TT1 #V2 #T2 #TT2 #IH #HV01 #HV02 #HT01 #HT02 #HTT1 #HTT2
-elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2
-elim (IH … HT01 … HT02) -HT01 HT02 IH // #T #HT1 #HT2
-elim (tpr_tps_bind … HV1 HT1 … HTT1) -HT1 HTT1 #U1 #TTU1 #HTU1
-elim (tpr_tps_bind … HV2 HT2 … HTT2) -HT2 HTT2 #U2 #TTU2 #HTU2
-elim (tps_conf_eq … HTU1 … HTU2) -HTU1 HTU2 #U #HU1 #HU2
+elim (IH … HV01 … HV02) -HV01 -HV02 // #V #HV1 #HV2
+elim (IH … HT01 … HT02) -HT01 -HT02 -IH // #T #HT1 #HT2
+elim (tpr_tps_bind … HV1 HT1 … HTT1) -T1 #U1 #TTU1 #HTU1
+elim (tpr_tps_bind … HV2 HT2 … HTT2) -T2 #U2 #TTU2 #HTU2
+elim (tps_conf_eq … HTU1 … HTU2) -T #U #HU1 #HU2
 @ex2_1_intro [2,3: @tpr_delta |1: skip ] /width=10/ (**) (* /3 width=10/ is too slow *)
 qed.
 
@@ -146,9 +146,9 @@ fact tpr_conf_delta_zeta:
    ∃∃X. 𝕓{Abbr} V1. TT1 ⇒ X & X2 ⇒ X.
 #X2 #V0 #V1 #T0 #T1 #TT1 #T2 #IH #_ #HT01 #HTT1 #HTX2 #HTT20
 elim (tpr_inv_lift … HT01 … HTT20) -HT01 #TT2 #HTT21 #HTT2
-lapply (tps_inv_lift1_eq … HTT1 … HTT21) -HTT1 #HTT1 destruct -T1;
+lapply (tps_inv_lift1_eq … HTT1 … HTT21) -HTT1 #HTT1 destruct
 lapply (tw_lift … HTT20) -HTT20 #HTT20
-elim (IH … HTX2 … HTT2) -HTX2 HTT2 IH /3/
+elim (IH … HTX2 … HTT2) -HTX2 -HTT2 -IH // /3 width=3/
 qed.
 
 (* Basic_1: was: pr0_upsilon_upsilon *)
@@ -162,12 +162,12 @@ fact tpr_conf_theta_theta:
    ↑[O, 1] V1 ≡ VV1 → ↑[O, 1] V2 ≡ VV2 →
    ∃∃X. 𝕔{Abbr} W1. 𝕔{Appl} VV1. T1 ⇒ X & 𝕔{Abbr} W2. 𝕔{Appl} VV2. T2 ⇒ X.
 #VV1 #V0 #V1 #W0 #W1 #T0 #T1 #V2 #VV2 #W2 #T2 #IH #HV01 #HV02 #HW01 #HW02 #HT01 #HT02 #HVV1 #HVV2
-elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2
-elim (IH … HW01 … HW02) -HW01 HW02 // #W #HW1 #HW2
-elim (IH … HT01 … HT02) -HT01 HT02 IH // #T #HT1 #HT2
+elim (IH … HV01 … HV02) -HV01 -HV02 // #V #HV1 #HV2
+elim (IH … HW01 … HW02) -HW01 -HW02 // #W #HW1 #HW2
+elim (IH … HT01 … HT02) -HT01 -HT02 -IH // #T #HT1 #HT2
 elim (lift_total V 0 1) #VV #HVV
-lapply (tpr_lift … HV1 … HVV1 … HVV) -HV1 HVV1 #HVV1
-lapply (tpr_lift … HV2 … HVV2 … HVV) -HV2 HVV2 HVV #HVV2
+lapply (tpr_lift … HV1 … HVV1 … HVV) -V1 #HVV1
+lapply (tpr_lift … HV2 … HVV2 … HVV) -V2 -HVV #HVV2
 @ex2_1_intro [2,3: @tpr_bind |1:skip ] /2 width=5/ (**) (* /4 width=5/ is too slow *)
 qed.
 
@@ -181,9 +181,9 @@ fact tpr_conf_zeta_zeta:
    ↑[O, 1] T0 ≡ TT0 → ↑[O, 1] T2 ≡ TT0 →
    ∃∃X. T1 ⇒ X & X2 ⇒ X.
 #V0 #X2 #TT0 #T0 #T1 #T2 #IH #HT01 #HTX2 #HTT0 #HTT20
-lapply (lift_inj … HTT0 … HTT20) -HTT0 #H destruct -T0;
+lapply (lift_inj … HTT0 … HTT20) -HTT0 #H destruct
 lapply (tw_lift … HTT20) -HTT20 #HTT20
-elim (IH … HT01 … HTX2) -HT01 HTX2 IH /2/
+elim (IH … HT01 … HTX2) -HT01 -HTX2 -IH // /2 width=3/
 qed.
 
 fact tpr_conf_tau_tau:
@@ -195,7 +195,7 @@ fact tpr_conf_tau_tau:
    T0 ⇒ T1 → T0 ⇒ X2 →
    ∃∃X. T1 ⇒ X & X2 ⇒ X.
 #V0 #T0 #X2 #T1 #IH #HT01 #HT02
-elim (IH … HT01 … HT02) -HT01 HT02 IH /2/
+elim (IH … HT01 … HT02) -HT01 -HT02 -IH // /2 width=3/
 qed.
 
 (* Confluence ***************************************************************)
@@ -208,70 +208,70 @@ fact tpr_conf_aux:
          ) →
    ∀X0,X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → X0 = Y0 →
    ∃∃X. X1 ⇒ X & X2 ⇒ X.
-#Y0 #IH #X0 #X1 #X2 * -X0 X1
-[ #I1 #H1 #H2 destruct -Y0;
+#Y0 #IH #X0 #X1 #X2 * -X0 -X1
+[ #I1 #H1 #H2 destruct
   lapply (tpr_inv_atom1 … H1) -H1
 (* case 1: atom, atom *)
-  #H1 destruct -X2 //
-| #I #V0 #V1 #T0 #T1 #HV01 #HT01 #H1 #H2 destruct -Y0;
+  #H1 destruct //
+| #I #V0 #V1 #T0 #T1 #HV01 #HT01 #H1 #H2 destruct
   elim (tpr_inv_flat1 … H1) -H1 *
 (* case 2: flat, flat *)
-  [ #V2 #T2 #HV02 #HT02 #H destruct -X2
+  [ #V2 #T2 #HV02 #HT02 #H destruct
     /3 width=7 by tpr_conf_flat_flat/ (**) (* /3 width=7/ is too slow *)
 (* case 3: flat, beta *)
-  | #V2 #W #U0 #T2 #HV02 #HT02 #H1 #H2 #H3 destruct -T0 X2 I
+  | #V2 #W #U0 #T2 #HV02 #HT02 #H1 #H2 #H3 destruct
     /3 width=8 by tpr_conf_flat_beta/ (**) (* /3 width=8/ is too slow *)
 (* case 4: flat, theta *)
-  | #V2 #V #W0 #W2 #U0 #U2 #HV02 #HW02 #HT02 #HV2 #H1 #H2 #H3 destruct -T0 X2 I
+  | #V2 #V #W0 #W2 #U0 #U2 #HV02 #HW02 #HT02 #HV2 #H1 #H2 #H3 destruct
     /3 width=11 by tpr_conf_flat_theta/ (**) (* /3 width=11/ is too slow *)
 (* case 5: flat, tau *)
-  | #HT02 #H destruct -I
+  | #HT02 #H destruct
     /3 width=6 by tpr_conf_flat_cast/ (**) (* /3 width=6/ is too slow *)
   ]
-| #V0 #V1 #W0 #T0 #T1 #HV01 #HT01 #H1 #H2 destruct -Y0;
+| #V0 #V1 #W0 #T0 #T1 #HV01 #HT01 #H1 #H2 destruct
   elim (tpr_inv_appl1 … H1) -H1 *
 (* case 6: beta, flat (repeated) *)
-  [ #V2 #T2 #HV02 #HT02 #H destruct -X2
+  [ #V2 #T2 #HV02 #HT02 #H destruct
     @ex2_1_comm /3 width=8 by tpr_conf_flat_beta/
 (* case 7: beta, beta *)
-  | #V2 #WW0 #TT0 #T2 #HV02 #HT02 #H1 #H2 destruct -W0 T0 X2
+  | #V2 #WW0 #TT0 #T2 #HV02 #HT02 #H1 #H2 destruct
     /3 width=8 by tpr_conf_beta_beta/ (**) (* /3 width=8/ is too slow *)
 (* case 8, beta, theta (excluded) *)
   | #V2 #VV2 #WW0 #W2 #TT0 #T2 #_ #_ #_ #_ #H destruct
   ]
-| #I1 #V0 #V1 #T0 #T1 #TT1 #HV01 #HT01 #HTT1 #H1 #H2 destruct -Y0;
+| #I1 #V0 #V1 #T0 #T1 #TT1 #HV01 #HT01 #HTT1 #H1 #H2 destruct
   elim (tpr_inv_bind1 … H1) -H1 *
 (* case 9: delta, delta *)
-  [ #V2 #T2 #TT2 #HV02 #HT02 #HTT2 #H destruct -X2
+  [ #V2 #T2 #TT2 #HV02 #HT02 #HTT2 #H destruct
     /3 width=11 by tpr_conf_delta_delta/ (**) (* /3 width=11/ is too slow *)
 (* case 10: delta, zata *)
-  | #T2 #HT20 #HTX2 #H destruct -I1;
+  | #T2 #HT20 #HTX2 #H destruct
     /3 width=10 by tpr_conf_delta_zeta/ (**) (* /3 width=10/ is too slow *)
   ]
-| #VV1 #V0 #V1 #W0 #W1 #T0 #T1 #HV01 #HVV1 #HW01 #HT01 #H1 #H2 destruct -Y0;
+| #VV1 #V0 #V1 #W0 #W1 #T0 #T1 #HV01 #HVV1 #HW01 #HT01 #H1 #H2 destruct
   elim (tpr_inv_appl1 … H1) -H1 *
 (* case 11: theta, flat (repeated) *)
-  [ #V2 #T2 #HV02 #HT02 #H destruct -X2
+  [ #V2 #T2 #HV02 #HT02 #H destruct
     @ex2_1_comm /3 width=11 by tpr_conf_flat_theta/
 (* case 12: theta, beta (repeated) *)
   | #V2 #WW0 #TT0 #T2 #_ #_ #H destruct
 (* case 13: theta, theta *)
-  | #V2 #VV2 #WW0 #W2 #TT0 #T2 #V02 #HW02 #HT02 #HVV2 #H1 #H2 destruct -W0 T0 X2
+  | #V2 #VV2 #WW0 #W2 #TT0 #T2 #V02 #HW02 #HT02 #HVV2 #H1 #H2 destruct
     /3 width=14 by tpr_conf_theta_theta/ (**) (* /3 width=14/ is too slow *)
   ]
-| #V0 #TT0 #T0 #T1 #HTT0 #HT01 #H1 #H2 destruct -Y0;
+| #V0 #TT0 #T0 #T1 #HTT0 #HT01 #H1 #H2 destruct
   elim (tpr_inv_abbr1 … H1) -H1 *
 (* case 14: zeta, delta (repeated) *)
-  [ #V2 #T2 #TT2 #HV02 #HT02 #HTT2 #H destruct -X2
+  [ #V2 #T2 #TT2 #HV02 #HT02 #HTT2 #H destruct
     @ex2_1_comm /3 width=10 by tpr_conf_delta_zeta/
 (* case 15: zeta, zeta *)
   | #T2 #HTT20 #HTX2
     /3 width=9 by tpr_conf_zeta_zeta/ (**) (* /3 width=9/ is too slow *)
   ] 
-| #V0 #T0 #T1 #HT01 #H1 #H2 destruct -Y0;
+| #V0 #T0 #T1 #HT01 #H1 #H2 destruct
   elim (tpr_inv_cast1 … H1) -H1
 (* case 16: tau, flat (repeated) *)
-  [ * #V2 #T2 #HV02 #HT02 #H destruct -X2
+  [ * #V2 #T2 #HV02 #HT02 #H destruct
     @ex2_1_comm /3 width=6 by tpr_conf_flat_cast/
 (* case 17: tau, tau *)
   | #HT02
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpss.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpss.ma
index f640d1326..e043031bd 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpss.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpss.ma
@@ -24,54 +24,54 @@ lemma tpr_tps_ltpr: ∀T1,T2. T1 ⇒ T2 →
                     ∀L1,d,e,U1. L1 ⊢ T1 [d, e] ≫ U1 →
                     ∀L2. L1 ⇒ L2 →
                     ∃∃U2. U1 ⇒ U2 & L2 ⊢ T2 [d, e] ≫* U2.
-#T1 #T2 #H elim H -H T1 T2
+#T1 #T2 #H elim H -T1 -T2
 [ #I #L1 #d #e #X #H
   elim (tps_inv_atom1 … H) -H
-  [ #H destruct -X /2/
-  | * #K1 #V1 #i #Hdi #Hide #HLK1 #HVU1 #H #L2 #HL12 destruct -I;
-    elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 HL12 #X #HLK2 #H
-    elim (ltpr_inv_pair1 … H) -H #K2 #V2 #_ #HV12 #H destruct -X;
+  [ #H destruct /2 width=3/
+  | * #K1 #V1 #i #Hdi #Hide #HLK1 #HVU1 #H #L2 #HL12 destruct
+    elim (ltpr_ldrop_conf … HLK1 … HL12) -L1 #X #HLK2 #H
+    elim (ltpr_inv_pair1 … H) -H #K2 #V2 #_ #HV12 #H destruct
     elim (lift_total V2 0 (i+1)) #U2 #HVU2
-    lapply (tpr_lift … HV12 … HVU1 … HVU2) -HV12 HVU1 #HU12
-    @ex2_1_intro [2: @HU12 | skip | /3/ ] (**) (* /4 width=6/ is too slow *)
+    lapply (tpr_lift … HV12 … HVU1 … HVU2) -V1 #HU12
+    @ex2_1_intro [2: @HU12 | skip | /3 width=4/ ] (**) (* /4 width=6/ is too slow *)
   ]
 | #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12
-  elim (tps_inv_flat1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct -X;
-  elim (IHV12 … HVW1 … HL12) -IHV12 HVW1;
-  elim (IHT12 … HTU1 … HL12) -IHT12 HTU1 HL12 /3 width=5/
+  elim (tps_inv_flat1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct
+  elim (IHV12 … HVW1 … HL12) -V1
+  elim (IHT12 … HTU1 … HL12) -T1 -HL12 /3 width=5/
 | #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12
-  elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct -X;
-  elim (tps_inv_bind1 … HY) -HY #WW #TT1 #_ #HTT1 #H destruct -Y;
-  elim (IHV12 … HVV1 … HL12) -IHV12 HVV1 #VV2 #HVV12 #HVV2
-  elim (IHT12 … HTT1 (L2. 𝕓{Abst} WW) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2
+  elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct
+  elim (tps_inv_bind1 … HY) -HY #WW #TT1 #_ #HTT1 #H destruct
+  elim (IHV12 … HVV1 … HL12) -V1 #VV2 #HVV12 #HVV2
+  elim (IHT12 … HTT1 (L2. 𝕓{Abst} WW) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2
   lapply (tpss_lsubs_conf … HTT2 (L2. 𝕓{Abbr} VV2) ?) -HTT2 /3 width=5/
 | #I #V1 #V2 #T1 #T2 #U2 #HV12 #_ #HTU2 #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12
-  elim (tps_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct -X;
-  elim (IHV12 … HVV1 … HL12) -IHV12 HVV1 #VV2 #HVV12 #HVV2
-  elim (IHT12 … HTT1 (L2. 𝕓{I} VV2) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2
-  elim (tpss_strip_neq … HTT2 … HTU2 ?) -HTT2 HTU2 T2 /2/ #T2 #HTT2 #HUT2
-  lapply (tps_lsubs_conf … HTT2 (L2. 𝕓{I} V2) ?) -HTT2 /2/ #HTT2
-  elim (ltpss_tps_conf … HTT2 (L2. 𝕓{I} VV2) (d + 1) e ?) -HTT2 /2/ #W2 #HTTW2 #HTW2 
-  lapply (tpss_lsubs_conf … HTTW2 (⋆. 𝕓{I} VV2) ?) -HTTW2 /2/ #HTTW2
+  elim (tps_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct
+  elim (IHV12 … HVV1 … HL12) -V1 #VV2 #HVV12 #HVV2
+  elim (IHT12 … HTT1 (L2. 𝕓{I} VV2) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2
+  elim (tpss_strip_neq … HTT2 … HTU2 ?) -T2 /2 width=1/ #T2 #HTT2 #HUT2
+  lapply (tps_lsubs_conf … HTT2 (L2. 𝕓{I} V2) ?) -HTT2 /2 width=1/ #HTT2
+  elim (ltpss_tps_conf … HTT2 (L2. 𝕓{I} VV2) (d + 1) e ?) -HTT2 /2 width=1/ #W2 #HTTW2 #HTW2
+  lapply (tpss_lsubs_conf … HTTW2 (⋆. 𝕓{I} VV2) ?) -HTTW2 /2 width=1/ #HTTW2
   lapply (tpss_tps … HTTW2) -HTTW2 #HTTW2
-  lapply (tpss_lsubs_conf … HTW2 (L2. 𝕓{I} VV2) ?) -HTW2 /2/ #HTW2
-  lapply (tpss_trans_eq … HUT2 … HTW2) -HUT2 HTW2 /3 width=5/
+  lapply (tpss_lsubs_conf … HTW2 (L2. 𝕓{I} VV2) ?) -HTW2 /2 width=1/ #HTW2
+  lapply (tpss_trans_eq … HUT2 … HTW2) -T2 /3 width=5/
 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #L1 #d #e #X #H #L2 #HL12
-  elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct -X;
-  elim (tps_inv_bind1 … HY) -HY #WW1 #TT1 #HWW1 #HTT1 #H destruct -Y;
-  elim (IHV12 … HVV1 … HL12) -IHV12 HVV1 #VV2 #HVV12 #HVV2
-  elim (IHW12 … HWW1 … HL12) -IHW12 HWW1 #WW2 #HWW12 #HWW2
-  elim (IHT12 … HTT1 (L2. 𝕓{Abbr} WW2) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2
+  elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct
+  elim (tps_inv_bind1 … HY) -HY #WW1 #TT1 #HWW1 #HTT1 #H destruct
+  elim (IHV12 … HVV1 … HL12) -V1 #VV2 #HVV12 #HVV2
+  elim (IHW12 … HWW1 … HL12) -W1 #WW2 #HWW12 #HWW2
+  elim (IHT12 … HTT1 (L2. 𝕓{Abbr} WW2) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2
   elim (lift_total VV2 0 1) #VV #H2VV
-  lapply (tpss_lift_ge … HVV2 (L2. 𝕓{Abbr} WW2) … HV2 … H2VV) -HVV2 HV2 /2/ #HVV
+  lapply (tpss_lift_ge … HVV2 (L2. 𝕓{Abbr} WW2) … HV2 … H2VV) -V2 /2 width=1/ #HVV
   @ex2_1_intro [2: @tpr_theta |1: skip |3: @tpss_bind [2: @tpss_flat ] ] /width=11/ (**) (* /4 width=11/ is too slow *)
-| #V1 #TT1 #T1 #T2 #HT1 #_ #IHT12 #L1 #d #e #X #H #L2 #HL12
-  elim (tps_inv_bind1 … H) -H #V2 #TT2 #HV12 #HTT12 #H destruct -X;
-  elim (tps_inv_lift1_ge … HTT12 L1 … HT1 ?) -HTT12 HT1 /2/ #T2 #HT12 #HTT2
-  elim (IHT12 … HT12 … HL12) -IHT12 HT12 HL12 <minus_plus_m_m /3/
+| #V1 #TT1 #T1 #T2 #HTT1 #_ #IHT12 #L1 #d #e #X #H #L2 #HL12
+  elim (tps_inv_bind1 … H) -H #V2 #TT2 #HV12 #HTT12 #H destruct
+  elim (tps_inv_lift1_ge … HTT12 L1 … HTT1 ?) -TT1 /2 width=1/ #T2 #HT12 #HTT2
+  elim (IHT12 … HT12 … HL12) -T1 -HL12 <minus_plus_m_m /3 width=3/
 | #V1 #T1 #T2 #_ #IHT12 #L1 #d #e #X #H #L2 #HL12
-  elim (tps_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct -X;
-  elim (IHT12 … HTT1 … HL12) -IHT12 HTT1 HL12 /3/
+  elim (tps_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct
+  elim (IHT12 … HTT1 … HL12) -T1 -HL12 /3 width=3/
 ]
 qed.
 
@@ -79,16 +79,16 @@ lemma tpr_tps_bind: ∀I,V1,V2,T1,T2,U1. V1 ⇒ V2 → T1 ⇒ T2 →
                     ⋆. 𝕓{I} V1 ⊢ T1 [0, 1] ≫ U1 →
                     ∃∃U2. U1 ⇒ U2 & ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ U2.
 #I #V1 #V2 #T1 #T2 #U1 #HV12 #HT12 #HTU1
-elim (tpr_tps_ltpr … HT12 … HTU1 (⋆. 𝕓{I} V2) ?) -HT12 HTU1 /3/
+elim (tpr_tps_ltpr … HT12 … HTU1 (⋆. 𝕓{I} V2) ?) -T1 /2 width=1/ /3 width=3/
 qed.
 
 lemma tpr_tpss_ltpr: ∀L1,L2. L1 ⇒ L2 → ∀T1,T2. T1 ⇒ T2 →
                      ∀d,e,U1. L1 ⊢ T1 [d, e] ≫* U1 →
                      ∃∃U2. U1 ⇒ U2 & L2 ⊢ T2 [d, e] ≫* U2.
 #L1 #L2 #HL12 #T1 #T2 #HT12 #d #e #U1 #HTU1 @(tpss_ind … HTU1) -U1
-[ /2/
+[ /2 width=3/
 | -HT12 #U #U1 #_ #HU1 * #T #HUT #HT2
-  elim (tpr_tps_ltpr … HUT … HU1 … HL12) -HUT HU1 HL12 #U2 #HU12 #HTU2
-  lapply (tpss_trans_eq … HT2 … HTU2) -T /2/
+  elim (tpr_tps_ltpr … HUT … HU1 … HL12) -U -HL12 #U2 #HU12 #HTU2
+  lapply (tpss_trans_eq … HT2 … HTU2) -T /2 width=3/
 ]
 qed.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/trf.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/trf.ma
index 96d678716..24b9e43f5 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/trf.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/trf.ma
@@ -53,12 +53,12 @@ fact trf_inv_atom_aux: ∀I,T. ℝ[T] → T =  𝕒{I} → False.
 qed.
 
 lemma trf_inv_atom: ∀I. ℝ[𝕒{I}] → False.
-/2/ qed-.
+/2 width=4/ qed-.
 
 fact trf_inv_abst_aux: ∀W,U,T. ℝ[T] → T =  𝕔{Abst} W. U → ℝ[W] ∨ ℝ[U].
 #W #U #T * -T
-[ #V #T #HV #H destruct -V T /2/
-| #V #T #HT #H destruct -V T /2/
+[ #V #T #HV #H destruct /2 width=1/
+| #V #T #HT #H destruct /2 width=1/
 | #V #T #_ #H destruct
 | #V #T #_ #H destruct
 | #V #T #H destruct
@@ -68,51 +68,51 @@ fact trf_inv_abst_aux: ∀W,U,T. ℝ[T] → T =  𝕔{Abst} W. U → ℝ[W] ∨
 qed.
 
 lemma trf_inv_abst: ∀V,T. ℝ[𝕔{Abst}V.T] → ℝ[V] ∨ ℝ[T].
-/2/ qed-.
+/2 width=3/ qed-.
 
 fact trf_inv_appl_aux: ∀W,U,T. ℝ[T] → T =  𝕔{Appl} W. U →
                        ∨∨ ℝ[W] | ℝ[U] | (𝕊[U] → False).
 #W #U #T * -T
 [ #V #T #_ #H destruct
 | #V #T #_ #H destruct
-| #V #T #HV #H destruct -V T /2/
-| #V #T #HT #H destruct -V T /2/
+| #V #T #HV #H destruct /2 width=1/
+| #V #T #HT #H destruct /2 width=1/
 | #V #T #H destruct
 | #V #T #H destruct
-| #V #W0 #T #H destruct -V U
+| #V #W0 #T #H destruct
   @or3_intro2 #H elim (simple_inv_bind … H)
 ]
 qed.
 
 lemma trf_inv_appl: ∀W,U. ℝ[𝕔{Appl}W.U] → ∨∨ ℝ[W] | ℝ[U] | (𝕊[U] → False).
-/2/ qed-.
+/2 width=3/ qed-.
 
 lemma tif_inv_abbr: ∀V,T. 𝕀[𝕔{Abbr}V.T] → False.
-/2/ qed-.
+/2 width=1/ qed-.
 
 lemma tif_inv_abst: ∀V,T. 𝕀[𝕔{Abst}V.T] → 𝕀[V] ∧ 𝕀[T].
-/4/ qed-.
+/4 width=1/ qed-.
 
 lemma tif_inv_appl: ∀V,T. 𝕀[𝕔{Appl}V.T] → ∧∧ 𝕀[V] & 𝕀[T] & 𝕊[T].
-#V #T #HVT @and3_intro /3/
-generalize in match HVT -HVT; elim T -T //
-* // * #U #T #_ #_ #H elim (H ?) -H /2/
+#V #T #HVT @and3_intro /3 width=1/
+generalize in match HVT; -HVT elim T -T //
+* // * #U #T #_ #_ #H elim (H ?) -H /2 width=1/
 qed-.
 
 lemma tif_inv_cast: ∀V,T. 𝕀[𝕔{Cast}V.T] → False.
-/2/ qed-.
+/2 width=1/ qed-.
 
 (* Basic properties *********************************************************)
 
 lemma tif_atom: ∀I. 𝕀[𝕒{I}].
-/2/ qed.
+/2 width=4/ qed.
 
 lemma tif_abst: ∀V,T. 𝕀[V] →  𝕀[T] →  𝕀[𝕔 {Abst}V.T].
 #V #T #HV #HT #H
-elim (trf_inv_abst … H) -H /2/
+elim (trf_inv_abst … H) -H /2 width=1/
 qed.
 
 lemma tif_appl: ∀V,T. 𝕀[V] →  𝕀[T] →  𝕊[T] → 𝕀[𝕔{Appl}V.T].
 #V #T #HV #HT #S #H
-elim (trf_inv_appl … H) -H /2/
+elim (trf_inv_appl … H) -H /2 width=1/
 qed.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/twhnf.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/twhnf.ma
index ccfaa6aa6..fe6b66447 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/twhnf.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/twhnf.ma
@@ -26,22 +26,22 @@ interpretation
 (* Basic inversion lemmas ***************************************************)
 
 lemma twhnf_inv_thom: ∀T. 𝕎ℍℕ[T] → T ≈ T.
-normalize /2 depth=1/
+normalize /2 width=1/
 qed-.
 
 (* Basic properties *********************************************************)
 
 lemma tpr_thom: ∀T1,T2. T1 ⇒ T2 → T1 ≈ T1 → T1 ≈ T2.
-#T1 #T2 #H elim H -T1 T2 //
+#T1 #T2 #H elim H -T1 -T2 //
 [ #I #V1 #V2 #T1 #T2 #_ #_ #_ #IHT12 #H
-  elim (thom_inv_flat1 … H) -H #W2 #U2 #HT1U2 #HT1 #_ #H1 #H2 destruct -I T1 V1;
-  lapply (IHT12 HT1U2) -IHT12 HT1U2 #HUT2
+  elim (thom_inv_flat1 … H) -H #W2 #U2 #HT1U2 #HT1 #_ #H1 #H2 destruct
+  lapply (IHT12 HT1U2) -IHT12 -HT1U2 #HUT2
   lapply (simple_thom_repl_dx … HUT2 HT1) /2 width=1/
 | #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #H
   elim (thom_inv_flat1 … H) -H #W2 #U2 #_ #H
   elim (simple_inv_bind … H)
 | #I #V1 #V2 #T1 #T #T2 #_ #_ #_ #_ #_ #H
-  elim (thom_inv_bind1 … H) -H #W2 #U2 #H destruct -I //
+  elim (thom_inv_bind1 … H) -H #W2 #U2 #H destruct //
 | #V2 #V1 #V #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H
   elim (thom_inv_flat1 … H) -H #U1 #U2 #_ #H
   elim (simple_inv_bind … H)
@@ -53,4 +53,4 @@ lemma tpr_thom: ∀T1,T2. T1 ⇒ T2 → T1 ≈ T1 → T1 ≈ T2.
 qed.
 
 lemma twhnf_thom: ∀T. T ≈ T → 𝕎ℍℕ[T].
-/2/ qed.
+/2 width=1/ qed.