From 7aa41e02e64bd09df253cc4267a44b4f49b16e03 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 26 Nov 2011 17:34:17 +0000
Subject: [PATCH] component "unfold" updated to new syntax ...

---
 .../lambda_delta/Basic_2/unfold/ltpss.ma      | 20 ++++---
 .../Basic_2/unfold/ltpss_ldrop.ma             | 20 +++----
 .../Basic_2/unfold/ltpss_ltpss.ma             | 14 ++---
 .../lambda_delta/Basic_2/unfold/ltpss_tpss.ma | 52 +++++++++----------
 .../lambda_delta/Basic_2/unfold/tpss.ma       | 46 ++++++++--------
 .../lambda_delta/Basic_2/unfold/tpss_lift.ma  | 52 +++++++++----------
 .../lambda_delta/Basic_2/unfold/tpss_ltps.ma  | 43 +++++++--------
 .../lambda_delta/Basic_2/unfold/tpss_tpss.ma  | 30 +++++------
 8 files changed, 138 insertions(+), 139 deletions(-)

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss.ma
index eb02c3a06..7c86262d9 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss.ma
@@ -35,10 +35,10 @@ qed-.
 
 lemma ltpss_strap: ∀L1,L,L2,d,e.
                    L1 [d, e] ≫ L → L [d, e] ≫* L2 → L1 [d, e] ≫* L2. 
-/2/ qed.
+/2 width=3/ qed.
 
 lemma ltpss_refl: ∀L,d,e. L [d, e] ≫* L.
-/2/ qed.
+/2 width=1/ qed.
 
 (* Basic inversion lemmas ***************************************************)
 
@@ -49,15 +49,14 @@ qed-.
 
 lemma ltpss_inv_atom1: ∀d,e,L2. ⋆ [d, e] ≫* L2 → L2 = ⋆.
 #d #e #L2 #H @(ltpss_ind … H) -L2 //
-#L #L2 #_ #HL2 #IHL destruct -L
+#L #L2 #_ #HL2 #IHL destruct
 >(ltps_inv_atom1 … HL2) -HL2 //
 qed-.
 
-fact ltpss_inv_atom2_aux: ∀d,e,L1,L2.
-                          L1 [d, e] ≫* L2 → L2 = ⋆ → L1 = ⋆.
+fact ltpss_inv_atom2_aux: ∀d,e,L1,L2. L1 [d, e] ≫* L2 → L2 = ⋆ → L1 = ⋆.
 #d #e #L1 #L2 #H @(ltpss_ind … H) -L2 //
-#L2 #L #_ #HL2 #IHL2 #H destruct -L;
-lapply (ltps_inv_atom2 … HL2) -HL2 /2/
+#L2 #L #_ #HL2 #IHL2 #H destruct
+lapply (ltps_inv_atom2 … HL2) -HL2 /2 width=1/
 qed.
 
 lemma ltpss_inv_atom2: ∀d,e,L1. L1 [d, e] ≫* ⋆ → L1 = ⋆.
@@ -71,7 +70,7 @@ fact ltps_inv_tps22_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → d = 0 → 0 < e →
 #d #e #L1 #L2 * -d e L1 L2
 [ #d #e #_ #_ #K1 #I #V1 #H destruct
 | #L1 #I #V #_ #H elim (lt_refl_false … H)
-| #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #_ #_ #K2 #J #W2 #H destruct -L2 I V2 /2 width=5/
+| #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #_ #_ #K2 #J #W2 #H destruct /2 width=5/
 | #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H elim (plus_S_eq_O_false … H)
 ]
 qed.
@@ -90,8 +89,7 @@ fact ltps_inv_tps12_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → 0 < d →
 [ #d #e #_ #I #K2 #V2 #H destruct
 | #L #I #V #H elim (lt_refl_false … H)
 | #L1 #L2 #I #V1 #V2 #e #_ #_ #H elim (lt_refl_false … H)
-| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #_ #J #K2 #W2 #H destruct -L2 I V2
-  /2 width=5/
+| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #_ #J #K2 #W2 #H destruct /2 width=5/
 ]
 qed.
 
@@ -99,5 +97,5 @@ lemma ltps_inv_tps12: ∀L1,K2,I,V2,d,e. L1 [d, e] ≫ K2. 𝕓{I} V2 → 0 < d
                       ∃∃K1,V1. K1 [d - 1, e] ≫ K2 &
                                   K2 ⊢ V1 [d - 1, e] ≫ V2 &
                                   L1 = K1. 𝕓{I} V1.
-/2/ qed.
+/2 width=1/ qed.
 *)
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_ldrop.ma
index 14d529db8..c9a8dda93 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_ldrop.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_ldrop.ma
@@ -20,23 +20,23 @@ include "Basic_2/unfold/ltpss.ma".
 lemma ltpss_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ≫* L1 →
                            ∀L2,e2. ↓[0, e2] L0 ≡ L2 →
                            d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2.
-#L0 #L1 #d1 #e1 #H @(ltpss_ind … H) -L1 /3 width=6/
+#L0 #L1 #d1 #e1 #H @(ltpss_ind … H) -L1 // /3 width=6/
 qed.
 
 lemma ltpss_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≫* L0 →
                             ∀L2,e2. ↓[0, e2] L0 ≡ L2 →
                             d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2.
-#L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0 /3 width=6/
+#L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0 // /3 width=6/
 qed.
 
 lemma ltpss_ldrop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ≫* L1 →
                            ∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
                            ∃∃L. L2 [0, d1 + e1 - e2] ≫* L & ↓[0, e2] L1 ≡ L.
 #L0 #L1 #d1 #e1 #H @(ltpss_ind … H) -L1
-[ /2/
+[ /2 width=3/
 | #L #L1 #_ #HL1 #IHL #L2 #e2 #HL02 #Hd1e2 #He2de1
   elim (IHL … HL02 Hd1e2 He2de1) -L0 #L0 #HL20 #HL0
-  elim (ltps_ldrop_conf_be … HL1 … HL0 Hd1e2 He2de1) -L /3/
+  elim (ltps_ldrop_conf_be … HL1 … HL0 Hd1e2 He2de1) -L /3 width=3/
 ]
 qed.
 
@@ -44,10 +44,10 @@ lemma ltpss_ldrop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ≫* L0 →
                             ∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
                             ∃∃L. L [0, d1 + e1 - e2] ≫* L2 & ↓[0, e2] L1 ≡ L.
 #L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0
-[ /2/
+[ /2 width=3/
 | #L #L0 #_ #HL0 #IHL #L2 #e2 #HL02 #Hd1e2 #He2de1
   elim (ltps_ldrop_trans_be … HL0 … HL02 Hd1e2 He2de1) -L0 #L0 #HL02 #HL0
-  elim (IHL … HL0 Hd1e2 He2de1) -L /3/
+  elim (IHL … HL0 Hd1e2 He2de1) -L /3 width=3/
 ]
 qed.
 
@@ -55,10 +55,10 @@ lemma ltpss_ldrop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ≫* L1 →
                            ∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 →
                            ∃∃L. L2 [d1 - e2, e1] ≫* L & ↓[0, e2] L1 ≡ L.
 #L0 #L1 #d1 #e1 #H @(ltpss_ind … H) -L1
-[ /2/
+[ /2 width=3/
 | #L #L1 #_ #HL1 #IHL #L2 #e2 #HL02 #He2d1
   elim (IHL … HL02 He2d1) -L0 #L0 #HL20 #HL0
-  elim (ltps_ldrop_conf_le … HL1 … HL0 He2d1) -L /3/
+  elim (ltps_ldrop_conf_le … HL1 … HL0 He2d1) -L /3 width=3/
 ]
 qed.
 
@@ -66,9 +66,9 @@ lemma ltpss_ldrop_trans_le: ∀L1,L0,d1,e1. L1 [d1, e1] ≫* L0 →
                             ∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 →
                             ∃∃L. L [d1 - e2, e1] ≫* L2 & ↓[0, e2] L1 ≡ L.
 #L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0
-[ /2/
+[ /2 width=3/
 | #L #L0 #_ #HL0 #IHL #L2 #e2 #HL02 #He2d1
   elim (ltps_ldrop_trans_le … HL0 … HL02 He2d1) -L0 #L0 #HL02 #HL0
-  elim (IHL … HL0 He2d1) -L /3/
+  elim (IHL … HL0 He2d1) -L /3 width=3/
 ]
 qed.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_ltpss.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_ltpss.ma
index 9a023056d..e4291acf9 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_ltpss.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_ltpss.ma
@@ -20,14 +20,14 @@ include "Basic_2/unfold/ltpss_tpss.ma".
 
 theorem ltpss_trans_eq: ∀L1,L,L2,d,e.
                         L1 [d, e] ≫* L → L [d, e] ≫* L2 → L1 [d, e] ≫* L2. 
-/2/ qed.
+/2 width=3/ qed.
 
 lemma ltpss_tpss2: ∀L1,L2,I,V1,V2,e.
                    L1 [0, e] ≫* L2 → L2 ⊢ V1 [0, e] ≫* V2 →
                    L1. 𝕓{I} V1 [0, e + 1] ≫* L2. 𝕓{I} V2.
 #L1 #L2 #I #V1 #V2 #e #HL12 #H @(tpss_ind … H) -V2
-[ /2/
-| #V #V2 #_ #HV2 #IHV @(ltpss_trans_eq … IHV) /2/
+[ /2 width=1/
+| #V #V2 #_ #HV2 #IHV @(ltpss_trans_eq … IHV) /2 width=1/
 ]
 qed.
 
@@ -35,15 +35,15 @@ lemma ltpss_tpss2_lt: ∀L1,L2,I,V1,V2,e.
                       L1 [0, e - 1] ≫* L2 → L2 ⊢ V1 [0, e - 1] ≫* V2 →
                       0 < e → L1. 𝕓{I} V1 [0, e] ≫* L2. 𝕓{I} V2.
 #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He
->(plus_minus_m_m e 1) /2/
+>(plus_minus_m_m e 1) // /2 width=1/
 qed.
 
 lemma ltpss_tpss1: ∀L1,L2,I,V1,V2,d,e.
                    L1 [d, e] ≫* L2 → L2 ⊢ V1 [d, e] ≫* V2 →
                    L1. 𝕓{I} V1 [d + 1, e] ≫* L2. 𝕓{I} V2.
 #L1 #L2 #I #V1 #V2 #d #e #HL12 #H @(tpss_ind … H) -V2
-[ /2/
-| #V #V2 #_ #HV2 #IHV @(ltpss_trans_eq … IHV) /2/
+[ /2 width=1/
+| #V #V2 #_ #HV2 #IHV @(ltpss_trans_eq … IHV) /2 width=1/
 ]
 qed.
 
@@ -51,5 +51,5 @@ lemma ltpss_tpss1_lt: ∀L1,L2,I,V1,V2,d,e.
                       L1 [d - 1, e] ≫* L2 → L2 ⊢ V1 [d - 1, e] ≫* V2 →
                       0 < d → L1. 𝕓{I} V1 [d, e] ≫* L2. 𝕓{I} V2.
 #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd
->(plus_minus_m_m d 1) /2/
+>(plus_minus_m_m d 1) // /2 width=1/
 qed.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_tpss.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_tpss.ma
index af49f1c05..c75119b66 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_tpss.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_tpss.ma
@@ -24,28 +24,28 @@ lemma ltpss_tpss_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≫* L0 →
                            d1 + e1 ≤ d2 → L1 ⊢ T2 [d2, e2] ≫* U2.
 #L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0 //
 #L #L0 #_ #HL0 #IHL #T2 #U2 #d2 #e2 #HTU2 #Hde1d2
-lapply (ltps_tpss_trans_ge … HL0 HTU2) -HL0 HTU2 /2/
+lapply (ltps_tpss_trans_ge … HL0 HTU2) -HL0 -HTU2 /2 width=1/
 qed.
 
 lemma ltpss_tps_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≫* L0 →
                           ∀T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 →
                           d1 + e1 ≤ d2 → L1 ⊢ T2 [d2, e2] ≫* U2.
 #L1 #L0 #d1 #e1 #HL10 #T2 #U2 #d2 #e2 #HTU2 #Hde1d2
-@(ltpss_tpss_trans_ge … HL10 … Hde1d2) /2/ (**) (* /3 width=6/ is too slow *)
+@(ltpss_tpss_trans_ge … HL10 … Hde1d2) /2 width=1/ (**) (* /3 width=6/ is too slow *)
 qed.
 
 lemma ltpss_tpss_trans_eq: ∀L0,L1,d,e. L0 [d, e] ≫* L1 →
                            ∀T2,U2. L1 ⊢ T2 [d, e] ≫* U2 → L0 ⊢ T2 [d, e] ≫* U2.
 #L0 #L1 #d #e #H @(ltpss_ind … H) -L1
-[ /2/
+[ /2 width=1/
 | #L #L1 #_ #HL1 #IHL #T2 #U2 #HTU2
-  lapply (ltps_tpss_trans_eq … HL1 HTU2) -HL1 HTU2 /2/
+  lapply (ltps_tpss_trans_eq … HL1 HTU2) -HL1 -HTU2 /2 width=1/
 ]
 qed.
 
 lemma ltpss_tps_trans_eq: ∀L0,L1,d,e. L0 [d, e] ≫* L1 →
                           ∀T2,U2. L1 ⊢ T2 [d, e] ≫ U2 → L0 ⊢ T2 [d, e] ≫* U2.
-/3/ qed.
+/3 width=3/ qed.
 
 lemma ltpss_tpss_conf_ge: ∀L0,L1,T2,U2,d1,e1,d2,e2. d1 + e1 ≤ d2 → 
                           L0 ⊢ T2 [d2, e2] ≫* U2 → L0 [d1, e1] ≫* L1 →
@@ -53,7 +53,7 @@ lemma ltpss_tpss_conf_ge: ∀L0,L1,T2,U2,d1,e1,d2,e2. d1 + e1 ≤ d2 →
 #L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde1d2 #HTU2 #H @(ltpss_ind … H) -L1
 [ //
 | -HTU2 #L #L1 #_ #HL1 #IHL
-  lapply (ltps_tpss_conf_ge … HL1 IHL) -HL1 IHL //
+  lapply (ltps_tpss_conf_ge … HL1 IHL) -HL1 -IHL //
 ]
 qed.
 
@@ -61,45 +61,45 @@ lemma ltpss_tps_conf_ge: ∀L0,L1,T2,U2,d1,e1,d2,e2. d1 + e1 ≤ d2 →
                          L0 ⊢ T2 [d2, e2] ≫ U2 → L0 [d1, e1] ≫* L1 →
                          L1 ⊢ T2 [d2, e2] ≫* U2.
 #L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde1d2 #HTU2 #HL01
-@(ltpss_tpss_conf_ge … Hde1d2 … HL01) /2/ (**) (* /3 width=6/ is too slow *)
+@(ltpss_tpss_conf_ge … Hde1d2 … HL01) /2 width=1/ (**) (* /3 width=6/ is too slow *)
 qed.
 
 lemma ltpss_tpss_conf_eq: ∀L0,L1,T2,U2,d,e.
                           L0 ⊢ T2 [d, e] ≫* U2 → L0 [d, e] ≫* L1 →
                           ∃∃T. L1 ⊢ T2 [d, e] ≫* T & L1 ⊢ U2 [d, e] ≫* T.
 #L0 #L1 #T2 #U2 #d #e #HTU2 #H @(ltpss_ind … H) -L1
-[ /2/
+[ /2 width=3/
 | -HTU2 #L #L1 #_ #HL1 * #W2 #HTW2 #HUW2
   elim (ltps_tpss_conf … HL1 HTW2) -HTW2 #T #HT2 #HW2T
-  elim (ltps_tpss_conf … HL1 HUW2) -HL1 HUW2 #U #HU2 #HW2U
-  elim (tpss_conf_eq … HW2T … HW2U) -HW2T HW2U #V #HTV #HUV
-  lapply (tpss_trans_eq … HT2 … HTV) -T;
-  lapply (tpss_trans_eq … HU2 … HUV) -U /2/
+  elim (ltps_tpss_conf … HL1 HUW2) -HL1 -HUW2 #U #HU2 #HW2U
+  elim (tpss_conf_eq … HW2T … HW2U) -HW2T -HW2U #V #HTV #HUV
+  lapply (tpss_trans_eq … HT2 … HTV) -T
+  lapply (tpss_trans_eq … HU2 … HUV) -U /2 width=3/
 ]
 qed.
 
 lemma ltpss_tps_conf_eq: ∀L0,L1,T2,U2,d,e.
                          L0 ⊢ T2 [d, e] ≫ U2 → L0 [d, e] ≫* L1 →
                          ∃∃T. L1 ⊢ T2 [d, e] ≫* T & L1 ⊢ U2 [d, e] ≫* T.
-/3/ qed.
+/3 width=3/ qed.
 
 lemma ltpss_tpss_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≫* T2 →
                        ∀L2,ds,es. L1 [ds, es] ≫* L2 → 
                        ∃∃T. L2 ⊢ T1 [d, e] ≫* T & L1 ⊢ T2 [ds, es] ≫* T.
 #L1 #T1 #T2 #d #e #HT12 #L2 #ds #es #H @(ltpss_ind … H) -L2
-[ /3/
+[ /3 width=3/
 | #L #L2 #HL1 #HL2 * #T #HT1 #HT2
   elim (ltps_tpss_conf … HL2 HT1) -HT1 #T0 #HT10 #HT0
-  lapply (ltps_tpss_trans_eq … HL2 … HT0) -HL2 HT0 #HT0
-  lapply (ltpss_tpss_trans_eq … HL1 … HT0) -HL1 HT0 #HT0
-  lapply (tpss_trans_eq … HT2 … HT0) -T /2/
+  lapply (ltps_tpss_trans_eq … HL2 … HT0) -HL2 -HT0 #HT0
+  lapply (ltpss_tpss_trans_eq … HL1 … HT0) -HL1 -HT0 #HT0
+  lapply (tpss_trans_eq … HT2 … HT0) -T /2 width=3/
 ]
 qed.
 
 lemma ltpss_tps_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≫ T2 →
                       ∀L2,ds,es. L1 [ds, es] ≫* L2 → 
                       ∃∃T. L2 ⊢ T1 [d, e] ≫* T & L1 ⊢ T2 [ds, es] ≫* T.
-/3/ qed.
+/3 width=1/ qed.
 
 (* Advanced properties ******************************************************)
 
@@ -107,10 +107,10 @@ lemma ltpss_tps2: ∀L1,L2,I,e.
                   L1 [0, e] ≫* L2 → ∀V1,V2. L2 ⊢ V1 [0, e] ≫ V2 →
                   L1. 𝕓{I} V1 [0, e + 1] ≫* L2. 𝕓{I} V2.
 #L1 #L2 #I #e #H @(ltpss_ind … H) -L2
-[ /3/
+[ /3 width=1/
 | #L #L2 #_ #HL2 #IHL #V1 #V2 #HV12
   elim (ltps_tps_trans … HV12 … HL2) -HV12 #V #HV1 #HV2
-  lapply (IHL … HV1) -IHL HV1 #HL1
+  lapply (IHL … HV1) -IHL -HV1 #HL1
   @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
 ]
 qed.
@@ -119,17 +119,17 @@ lemma ltpss_tps2_lt: ∀L1,L2,I,V1,V2,e.
                      L1 [0, e - 1] ≫* L2 → L2 ⊢ V1 [0, e - 1] ≫ V2 →
                      0 < e → L1. 𝕓{I} V1 [0, e] ≫* L2. 𝕓{I} V2.
 #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He
->(plus_minus_m_m e 1) /2/
+>(plus_minus_m_m e 1) // /2 width=1/
 qed.
 
 lemma ltpss_tps1: ∀L1,L2,I,d,e. L1 [d, e] ≫* L2 →
                   ∀V1,V2. L2 ⊢ V1 [d, e] ≫ V2 →
                   L1. 𝕓{I} V1 [d + 1, e] ≫* L2. 𝕓{I} V2.
 #L1 #L2 #I #d #e #H @(ltpss_ind … H) -L2
-[ /3/
+[ /3 width=1/
 | #L #L2 #_ #HL2 #IHL #V1 #V2 #HV12
   elim (ltps_tps_trans … HV12 … HL2) -HV12 #V #HV1 #HV2
-  lapply (IHL … HV1) -IHL HV1 #HL1
+  lapply (IHL … HV1) -IHL -HV1 #HL1
   @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
 ]
 qed.
@@ -138,7 +138,7 @@ lemma ltpss_tps1_lt: ∀L1,L2,I,V1,V2,d,e.
                      L1 [d - 1, e] ≫* L2 → L2 ⊢ V1 [d - 1, e] ≫ V2 →
                      0 < d → L1. 𝕓{I} V1 [d, e] ≫* L2. 𝕓{I} V2.
 #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd
->(plus_minus_m_m d 1) /2/
+>(plus_minus_m_m d 1) // /2 width=1/
 qed.
 
 (* Advanced forward lemmas **************************************************)
@@ -148,7 +148,7 @@ lemma ltpss_fwd_tpss21: ∀e,K1,I,V1,L2. 0 < e → K1. 𝕓{I} V1 [0, e] ≫* L2
                                  L2 = K2. 𝕓{I} V2.
 #e #K1 #I #V1 #L2 #He #H @(ltpss_ind … H) -L2
 [ /2 width=5/
-| #L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct -L;
+| #L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct
   elim (ltps_inv_tps21 … HL2 ?) -HL2 // #K2 #V2 #HK2 #HV2 #H
   lapply (ltps_tps_trans_eq … HV2 … HK2) -HV2 #HV2
   lapply (ltpss_tpss_trans_eq … HK1 … HV2) -HV2 #HV2 /3 width=5/
@@ -161,7 +161,7 @@ lemma ltpss_fwd_tpss11: ∀d,e,I,K1,V1,L2. 0 < d → K1. 𝕓{I} V1 [d, e] ≫*
                                  L2 = K2. 𝕓{I} V2.
 #d #e #K1 #I #V1 #L2 #Hd #H @(ltpss_ind … H) -L2
 [ /2 width=5/
-| #L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct -L;
+| #L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct
   elim (ltps_inv_tps11 … HL2 ?) -HL2 // #K2 #V2 #HK2 #HV2 #H
   lapply (ltps_tps_trans_eq … HV2 … HK2) -HV2 #HV2
   lapply (ltpss_tpss_trans_eq … HK1 … HV2) -HV2 #HV2 /3 width=5/
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss.ma
index f21f3603e..98a8caa50 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss.ma
@@ -34,58 +34,58 @@ qed-.
 
 lemma tpss_strap: ∀L,T1,T,T2,d,e. 
                   L ⊢ T1 [d, e] ≫ T → L ⊢ T [d, e] ≫* T2 → L ⊢ T1 [d, e] ≫* T2. 
-/2/ qed.
+/2 width=3/ qed.
 
 lemma tpss_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≫* T2 →
                        ∀L2. L1 [d, e] ≼ L2 → L2 ⊢ T1 [d, e] ≫* T2.
-/3/ qed.
+/3 width=3/ qed.
 
 lemma tpss_refl: ∀d,e,L,T. L ⊢ T [d, e] ≫* T.
-/2/ qed.
+/2 width=1/ qed.
 
 lemma tpss_bind: ∀L,V1,V2,d,e. L ⊢ V1 [d, e] ≫* V2 →
                  ∀I,T1,T2. L. 𝕓{I} V2 ⊢ T1 [d + 1, e] ≫* T2 →
                  L ⊢ 𝕓{I} V1. T1 [d, e] ≫* 𝕓{I} V2. T2.
-#L #V1 #V2 #d #e #HV12 elim HV12 -HV12 V2
-[ #V2 #HV12 #I #T1 #T2 #HT12 elim HT12 -HT12 T2
+#L #V1 #V2 #d #e #HV12 elim HV12 -V2
+[ #V2 #HV12 #I #T1 #T2 #HT12 elim HT12 -T2
   [ /3 width=5/
   | #T #T2 #_ #HT2 #IHT @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
   ]
 | #V #V2 #_ #HV12 #IHV #I #T1 #T2 #HT12
-  lapply (tpss_lsubs_conf … HT12 (L. 𝕓{I} V) ?) -HT12 /2/ #HT12
-  lapply (IHV … HT12) -IHV HT12 #HT12 @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
+  lapply (tpss_lsubs_conf … HT12 (L. 𝕓{I} V) ?) -HT12 /2 width=1/ #HT12
+  lapply (IHV … HT12) -IHV -HT12 #HT12 @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
 ]
 qed.
 
 lemma tpss_flat: ∀L,I,V1,V2,T1,T2,d,e.
                  L ⊢ V1 [d, e] ≫ * V2 → L ⊢ T1 [d, e] ≫* T2 →
                  L ⊢ 𝕗{I} V1. T1 [d, e] ≫* 𝕗{I} V2. T2.
-#L #I #V1 #V2 #T1 #T2 #d #e #HV12 elim HV12 -HV12 V2
-[ #V2 #HV12 #HT12 elim HT12 -HT12 T2
-  [ /3/
+#L #I #V1 #V2 #T1 #T2 #d #e #HV12 elim HV12 -V2
+[ #V2 #HV12 #HT12 elim HT12 -T2
+  [ /3 width=1/
   | #T #T2 #_ #HT2 #IHT @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
   ]
 | #V #V2 #_ #HV12 #IHV #HT12
-  lapply (IHV … HT12) -IHV HT12 #HT12 @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
+  lapply (IHV … HT12) -IHV -HT12 #HT12 @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
 ]
 qed.
 
 lemma tpss_weak: ∀L,T1,T2,d1,e1. L ⊢ T1 [d1, e1] ≫* T2 →
                  ∀d2,e2. d2 ≤ d1 → d1 + e1 ≤ d2 + e2 →
                  L ⊢ T1 [d2, e2] ≫* T2.
-#L #T1 #T2 #d1 #e1 #H #d1 #d2 #Hd21 #Hde12 @(tpss_ind … H) -H T2
+#L #T1 #T2 #d1 #e1 #H #d1 #d2 #Hd21 #Hde12 @(tpss_ind … H) -T2
 [ //
 | #T #T2 #_ #HT12 #IHT
-  lapply (tps_weak … HT12 … Hd21 Hde12) -HT12 Hd21 Hde12 /2/
+  lapply (tps_weak … HT12 … Hd21 Hde12) -HT12 -Hd21 -Hde12 /2 width=3/
 ]
 qed.
 
 lemma tpss_weak_top: ∀L,T1,T2,d,e.
                      L ⊢ T1 [d, e] ≫* T2 → L ⊢ T1 [d, |L| - d] ≫* T2.
-#L #T1 #T2 #d #e #H @(tpss_ind … H) -H T2
+#L #T1 #T2 #d #e #H @(tpss_ind … H) -T2
 [ //
 | #T #T2 #_ #HT12 #IHT
-  lapply (tps_weak_top … HT12) -HT12 /2/
+  lapply (tps_weak_top … HT12) -HT12 /2 width=3/
 ]
 qed.
 
@@ -100,9 +100,9 @@ qed.
 
 (* Note: this can be derived from tpss_inv_atom1 *)
 lemma tpss_inv_sort1: ∀L,T2,k,d,e. L ⊢ ⋆k [d, e] ≫* T2 → T2 = ⋆k.
-#L #T2 #k #d #e #H @(tpss_ind … H) -H T2
+#L #T2 #k #d #e #H @(tpss_ind … H) -T2
 [ //
-| #T #T2 #_ #HT2 #IHT destruct -T
+| #T #T2 #_ #HT2 #IHT destruct
   >(tps_inv_sort1 … HT2) -HT2 //
 ]
 qed-.
@@ -111,26 +111,26 @@ lemma tpss_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕓{I} V1. T1 [d, e] ≫* U2 
                       ∃∃V2,T2. L ⊢ V1 [d, e] ≫* V2 & 
                                L. 𝕓{I} V2 ⊢ T1 [d + 1, e] ≫* T2 &
                                U2 =  𝕓{I} V2. T2.
-#d #e #L #I #V1 #T1 #U2 #H @(tpss_ind … H) -H U2
+#d #e #L #I #V1 #T1 #U2 #H @(tpss_ind … H) -U2
 [ /2 width=5/
-| #U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct -U;
+| #U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct
   elim (tps_inv_bind1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H
-  lapply (tpss_lsubs_conf … HT1 (L. 𝕓{I} V2) ?) -HT1 /3 width=5/
+  lapply (tpss_lsubs_conf … HT1 (L. 𝕓{I} V2) ?) -HT1 /2 width=1/ /3 width=5/
 ]
 qed-.
 
 lemma tpss_inv_flat1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕗{I} V1. T1 [d, e] ≫* U2 →
                       ∃∃V2,T2. L ⊢ V1 [d, e] ≫* V2 & L ⊢ T1 [d, e] ≫* T2 &
                                U2 =  𝕗{I} V2. T2.
-#d #e #L #I #V1 #T1 #U2 #H @(tpss_ind … H) -H U2
+#d #e #L #I #V1 #T1 #U2 #H @(tpss_ind … H) -U2
 [ /2 width=5/
-| #U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct -U;
+| #U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct
   elim (tps_inv_flat1 … HU2) -HU2 /3 width=5/
 ]
 qed-.
 
 lemma tpss_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 [d, 0] ≫* T2 → T1 = T2.
-#L #T1 #T2 #d #H @(tpss_ind … H) -H T2
+#L #T1 #T2 #d #H @(tpss_ind … H) -T2
 [ //
 | #T #T2 #_ #HT2 #IHT <(tps_inv_refl_O2 … HT2) -HT2 //
 ]
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_lift.ma
index 2ba57a9c5..53c4f0c68 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_lift.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_lift.ma
@@ -23,14 +23,14 @@ lemma tpss_subst: ∀L,K,V,U1,i,d,e.
                   d ≤ i → i < d + e →
                   ↓[0, i] L ≡ K. 𝕓{Abbr} V → K ⊢ V [0, d + e - i - 1] ≫* U1 →
                   ∀U2. ↑[0, i + 1] U1 ≡ U2 → L ⊢ #i [d, e] ≫* U2.
-#L #K #V #U1 #i #d #e #Hdi #Hide #HLK #H @(tpss_ind … H) -H U1
-[ /3/
+#L #K #V #U1 #i #d #e #Hdi #Hide #HLK #H @(tpss_ind … H) -U1
+[ /3 width=4/
 | #U #U1 #_ #HU1 #IHU #U2 #HU12
   elim (lift_total U 0 (i+1)) #U0 #HU0
   lapply (IHU … HU0) -IHU #H
   lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
-  lapply (tps_lift_ge … HU1 … HLK HU0 HU12 ?) -HU1 HLK HU0 HU12 // normalize #HU02
-  lapply (tps_weak … HU02 d e ? ?) -HU02 [ >arith_i2 // | /2/ | /2/ ]
+  lapply (tps_lift_ge … HU1 … HLK HU0 HU12 ?) -HU1 -HLK -HU0 -HU12 // normalize #HU02
+  lapply (tps_weak … HU02 d e ? ?) -HU02 [ >arith_i2 // | /2 width=1/ | /2 width=3/ ]
 ]
 qed.
 
@@ -43,15 +43,15 @@ lemma tpss_inv_atom1: ∀L,T2,I,d,e. L ⊢ 𝕒{I} [d, e] ≫* T2 →
                                    K ⊢ V1 [0, d + e - i - 1] ≫* V2 &
                                    ↑[O, i + 1] V2 ≡ T2 &
                                    I = LRef i.
-#L #T2 #I #d #e #H @(tpss_ind … H) -H T2
-[ /2/
+#L #T2 #I #d #e #H @(tpss_ind … H) -T2
+[ /2 width=1/
 | #T #T2 #_ #HT2 *
-  [ #H destruct -T;
-    elim (tps_inv_atom1 … HT2) -HT2 [ /2/ | * /3 width=10/ ]
+  [ #H destruct
+    elim (tps_inv_atom1 … HT2) -HT2 [ /2 width=1/ | * /3 width=10/ ]
   | * #K #V1 #V #i #Hdi #Hide #HLK #HV1 #HVT #HI
     lapply (ldrop_fwd_ldrop2 … HLK) #H
-    elim (tps_inv_lift1_up … HT2 … H … HVT ? ? ?) normalize -HT2 H HVT [2,3,4: /2/ ] #V2 <minus_plus #HV2 #HVT2
-    @or_intror @(ex6_4_intro … Hdi Hide HLK … HVT2 HI) /2/ (**) (* /4 width=10/ is too slow *)
+    elim (tps_inv_lift1_up … HT2 … H … HVT ? ? ?) normalize -HT2 -H -HVT [2,3,4: /2 width=1/ ] #V2 <minus_plus #HV2 #HVT2
+    @or_intror @(ex6_4_intro … Hdi Hide HLK … HVT2 HI) /2 width=3/ (**) (* /4 width=10/ is too slow *)
   ]
 ]
 qed-.
@@ -63,13 +63,13 @@ lemma tpss_inv_lref1: ∀L,T2,i,d,e. L ⊢ #i [d, e] ≫* T2 →
                                  K ⊢ V1 [0, d + e - i - 1] ≫* V2 &
                                  ↑[O, i + 1] V2 ≡ T2.
 #L #T2 #i #d #e #H
-elim (tpss_inv_atom1 … H) -H /2/
-* #K #V1 #V2 #j #Hdj #Hjde #HLK #HV12 #HVT2 #H destruct -i /3 width=6/
+elim (tpss_inv_atom1 … H) -H /2 width=1/
+* #K #V1 #V2 #j #Hdj #Hjde #HLK #HV12 #HVT2 #H destruct /3 width=6/
 qed-.
 
 lemma tpss_inv_refl_SO2: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ≫* T2 →
                          ∀K,V. ↓[0, d] L ≡ K. 𝕓{Abst} V → T1 = T2.
-#L #T1 #T2 #d #H #K #V #HLK @(tpss_ind … H) -H T2 //
+#L #T1 #T2 #d #H #K #V #HLK @(tpss_ind … H) -T2 //
 #T #T2 #_ #HT2 #IHT <(tps_inv_refl_SO2 … HT2 … HLK) //
 qed-.
 
@@ -84,7 +84,7 @@ lemma tpss_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫* T2 →
 | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
   elim (lift_total T d e) #U #HTU
   lapply (IHT … HTU) -IHT #HU1
-  lapply (tps_lift_le … HT2 … HLK HTU HTU2 ?) -HT2 HLK HTU HTU2 /2/
+  lapply (tps_lift_le … HT2 … HLK HTU HTU2 ?) -HT2 -HLK -HTU -HTU2 // /2 width=3/
 ]
 qed.
 
@@ -97,7 +97,7 @@ lemma tpss_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫* T2 →
 | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
   elim (lift_total T d e) #U #HTU
   lapply (IHT … HTU) -IHT #HU1
-  lapply (tps_lift_be … HT2 … HLK HTU HTU2 ? ?) -HT2 HLK HTU HTU2 /2/
+  lapply (tps_lift_be … HT2 … HLK HTU HTU2 ? ?) -HT2 -HLK -HTU -HTU2 // /2 width=3/
 ]
 qed.
 
@@ -110,7 +110,7 @@ lemma tpss_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫* T2 →
 | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
   elim (lift_total T d e) #U #HTU
   lapply (IHT … HTU) -IHT #HU1
-  lapply (tps_lift_ge … HT2 … HLK HTU HTU2 ?) -HT2 HLK HTU HTU2 /2/
+  lapply (tps_lift_ge … HT2 … HLK HTU HTU2 ?) -HT2 -HLK -HTU -HTU2 // /2 width=3/
 ]
 qed.
 
@@ -119,9 +119,9 @@ lemma tpss_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 →
                          dt + et ≤ d →
                          ∃∃T2. K ⊢ T1 [dt, et] ≫* T2 & ↑[d, e] T2 ≡ U2.
 #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdetd @(tpss_ind … H) -U2
-[ /2/
+[ /2 width=3/
 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
-  elim (tps_inv_lift1_le … HU2 … HLK … HTU ?) -HU2 HLK HTU // /3/
+  elim (tps_inv_lift1_le … HU2 … HLK … HTU ?) -HU2 -HLK -HTU // /3 width=3/
 ]
 qed.
 
@@ -130,9 +130,9 @@ lemma tpss_inv_lift1_be: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 →
                          dt ≤ d → d + e ≤ dt + et →
                          ∃∃T2. K ⊢ T1 [dt, et - e] ≫* T2 & ↑[d, e] T2 ≡ U2.
 #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdedet @(tpss_ind … H) -U2
-[ /2/
+[ /2 width=3/
 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
-  elim (tps_inv_lift1_be … HU2 … HLK … HTU ? ?) -HU2 HLK HTU // /3/
+  elim (tps_inv_lift1_be … HU2 … HLK … HTU ? ?) -HU2 -HLK -HTU // /3 width=3/
 ]
 qed.
 
@@ -141,17 +141,17 @@ lemma tpss_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 →
                          d + e ≤ dt →
                          ∃∃T2. K ⊢ T1 [dt - e, et] ≫* T2 & ↑[d, e] T2 ≡ U2.
 #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdedt @(tpss_ind … H) -U2
-[ /2/
+[ /2 width=3/
 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
-  elim (tps_inv_lift1_ge … HU2 … HLK … HTU ?) -HU2 HLK HTU // /3/
+  elim (tps_inv_lift1_ge … HU2 … HLK … HTU ?) -HU2 -HLK -HTU // /3 width=3/
 ]
 qed.
 
 lemma tpss_inv_lift1_eq: ∀L,U1,U2,d,e.
                          L ⊢ U1 [d, e] ≫* U2 → ∀T1. ↑[d, e] T1 ≡ U1 → U1 = U2.
 #L #U1 #U2 #d #e #H #T1 #HTU1 @(tpss_ind … H) -U2 //
-#U #U2 #_ #HU2 #IHU destruct -U1
-<(tps_inv_lift1_eq … HU2 … HTU1) -HU2 HTU1 //
+#U #U2 #_ #HU2 #IHU destruct
+<(tps_inv_lift1_eq … HU2 … HTU1) -HU2 -HTU1 //
 qed.
 
 lemma tpss_inv_lift1_be_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 →
@@ -159,8 +159,8 @@ lemma tpss_inv_lift1_be_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 →
                             dt ≤ d → dt + et ≤ d + e →
                             ∃∃T2. K ⊢ T1 [dt, d - dt] ≫* T2 & ↑[d, e] T2 ≡ U2.
 #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdetde @(tpss_ind … H) -U2
-[ /2/
+[ /2 width=3/
 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
-  elim (tps_inv_lift1_be_up … HU2 … HLK … HTU ? ?) -HU2 HLK HTU // /3/
+  elim (tps_inv_lift1_be_up … HU2 … HLK … HTU ? ?) -HU2 -HLK -HTU // /3 width=3/
 ]
 qed.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_ltps.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_ltps.ma
index abaf3f7c0..18b181741 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_ltps.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_ltps.ma
@@ -24,16 +24,16 @@ lemma ltps_tpss_conf_ge: ∀L0,L1,T2,U2,d1,e1,d2,e2.
                          L0 ⊢ T2 [d2, e2] ≫* U2 → L1 ⊢ T2 [d2, e2] ≫* U2.
 #L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde1d2 #HL01 #H @(tpss_ind … H) -U2 //
 #U #U2 #_ #HU2 #IHU
-lapply (ltps_tps_conf_ge … HU2 … HL01 ?) -HU2 HL01 /2/
+lapply (ltps_tps_conf_ge … HU2 … HL01 ?) -HU2 -HL01 // /2 width=3/
 qed.
 
 lemma ltps_tpss_conf: ∀L0,L1,T2,U2,d1,e1,d2,e2.
                       L0 [d1, e1] ≫ L1 → L0 ⊢ T2 [d2, e2] ≫* U2 →
                       ∃∃T. L1 ⊢ T2 [d2, e2] ≫* T & L1 ⊢ U2 [d1, e1] ≫* T.
 #L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #HL01 #H @(tpss_ind … H) -U2
-[ /3/
+[ /3 width=3/
 | #U #U2 #_ #HU2 * #T #HT2 #HUT
-  elim (ltps_tps_conf … HU2 … HL01) -HU2 HL01 #W #HUW #HU2W
+  elim (ltps_tps_conf … HU2 … HL01) -HU2 -HL01 #W #HUW #HU2W
   elim (tpss_strip_eq … HUT … HUW) -U
   /3 width=5 by ex2_1_intro, step, tpss_strap/ (**) (* just /3 width=5/ is too slow *)
 ]
@@ -44,42 +44,43 @@ lemma ltps_tpss_trans_ge: ∀L0,L1,T2,U2,d1,e1,d2,e2.
                           L0 ⊢ T2 [d2, e2] ≫* U2 → L1 ⊢ T2 [d2, e2] ≫* U2.
 #L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde1d2 #HL10 #H @(tpss_ind … H) -U2 //
 #U #U2 #_ #HU2 #IHU
-lapply (ltps_tps_trans_ge … HU2 … HL10 ?) -HU2 HL10 /2/
+lapply (ltps_tps_trans_ge … HU2 … HL10 ?) -HU2 -HL10 // /2 width=3/
 qed.
 
 lemma ltps_tpss_trans_down: ∀L0,L1,T2,U2,d1,e1,d2,e2. d2 + e2 ≤ d1 →
                             L1 [d1, e1] ≫ L0 → L0 ⊢ T2 [d2, e2] ≫* U2 →
                             ∃∃T. L1 ⊢ T2 [d2, e2] ≫* T & L0 ⊢ T [d1, e1] ≫* U2.
 #L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde2d1 #HL10 #H @(tpss_ind … H) -U2
-[ /3/
+[ /3 width=3/
 | #U #U2 #_ #HU2 * #T #HT2 #HTU
   elim (tpss_strap1_down … HTU … HU2 ?) -U // #U #HTU #HU2
-  elim (ltps_tps_trans … HTU … HL10) -HTU HL10 #W #HTW #HWU
-  @(ex2_1_intro … W) /2/ (**) (* /3 width=5/ does not work as in ltps_tpss_conf *)
+  elim (ltps_tps_trans … HTU … HL10) -HTU -HL10 #W #HTW #HWU
+  @(ex2_1_intro … W) /2 width=3/ (**) (* /3 width=5/ does not work as in ltps_tpss_conf *)
 ]
 qed.
 
 fact ltps_tps_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e.
                             L1 ⊢ T2 [d, e] ≫ U2 → ∀L0. L0 [d, e] ≫ L1 →
                             Y1 = L1 → X2 = T2 → L0 ⊢ T2 [d, e] ≫* U2.
-#Y1 #X2 @(cw_wf_ind … Y1 X2) -Y1 X2 #Y1 #X2 #IH
-#L1 #T2 #U2 #d #e * -L1 T2 U2 d e
+#Y1 #X2 @(cw_wf_ind … Y1 X2) -Y1 -X2 #Y1 #X2 #IH
+#L1 #T2 #U2 #d #e * -L1 -T2 -U2 -d -e
 [ //
-| #L1 #K1 #V1 #W1 #i #d #e #Hdi #Hide #HLK1 #HVW1 #L0 #HL10 #H1 #H2 destruct -Y1 X2;
+| #L1 #K1 #V1 #W1 #i #d #e #Hdi #Hide #HLK1 #HVW1 #L0 #HL10 #H1 #H2 destruct
   lapply (ldrop_fwd_lw … HLK1) normalize #H1
-  elim (ltps_ldrop_trans_be … HL10 … HLK1 ? ?) -HL10 HLK1 [2,3: /2/ ] #X #H #HLK0
-  elim (ltps_inv_tps22 … H ?) -H [2: /2/ ] #K0 #V0 #HK01 #HV01 #H destruct -X;
+  elim (ltps_ldrop_trans_be … HL10 … HLK1 ? ?) -HL10 -HLK1 /2 width=1/ #X #H #HLK0
+  elim (ltps_inv_tps22 … H ?) -H /2 width=1/ #K0 #V0 #HK01 #HV01 #H destruct
   lapply (tps_fwd_tw … HV01) #H2
-  lapply (transitive_le (#[K1] + #[V0]) … H1) -H1 [ /2/ ] -H2 #H
-  lapply (IH … HV01 … HK01 ? ?) -IH HV01 HK01 [1,3: // |2,4: skip | normalize /2/ | /3 width=6/ ]
-| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #L0 #HL0 #H1 #H2 destruct -Y1 X2;
-  lapply (tps_lsubs_conf … HT12 (L. 𝕓{I} V1) ?) -HT12 /2/ #HT12
+  lapply (transitive_le (#[K1] + #[V0]) … H1) -H1 /2 width=1/ -H2 #H
+  lapply (IH … HV01 … HK01 ? ?) -IH -HV01 -HK01
+  [1,3: // |2,4: skip | normalize /2 width=1/ | /3 width=6/ ]
+| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #L0 #HL0 #H1 #H2 destruct
+  lapply (tps_lsubs_conf … HT12 (L. 𝕓{I} V1) ?) -HT12 /2 width=1/ #HT12
   lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3,5: normalize // |2,4: skip ] #HV12
-  lapply (IH … HT12 (L0. 𝕓{I} V1) ? ? ?) -IH HT12 [1,3,5: /2/ |2,4: skip | normalize // ] -HL0 #HT12
-  lapply (tpss_lsubs_conf … HT12 (L0. 𝕓{I} V2) ?) -HT12 /2/
-| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #L0 #HL0 #H1 #H2 destruct -Y1 X2;
+  lapply (IH … HT12 (L0. 𝕓{I} V1) ? ? ?) -IH -HT12 [1,3,5: /2 width=2/ |2,4: skip | normalize // ] -HL0 #HT12
+  lapply (tpss_lsubs_conf … HT12 (L0. 𝕓{I} V2) ?) -HT12 /2 width=1/
+| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #L0 #HL0 #H1 #H2 destruct
   lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3,5: normalize // |2,4: skip ]
-  lapply (IH … HT12 … HL0 ? ?) -IH HT12 [1,3,5: normalize // |2,4: skip ] -HL0 /2/
+  lapply (IH … HT12 … HL0 ? ?) -IH -HT12 [1,3,5: normalize // |2,4: skip ] -HL0 /2 width=1/
 ]
 qed.
 
@@ -90,5 +91,5 @@ lemma ltps_tps_trans_eq: ∀L1,T2,U2,d,e. L1 ⊢ T2 [d, e] ≫ U2 →
 lemma ltps_tpss_trans_eq: ∀L0,L1,T2,U2,d,e. L0 [d, e] ≫ L1 →
                           L1 ⊢ T2 [d, e] ≫* U2 → L0 ⊢ T2 [d, e] ≫* U2.
 #L0 #L1 #T2 #U2 #d #e #HL01 #H @(tpss_ind … H) -U2 //
-#U #U2 #_ #HU2 #IHU @(tpss_trans_eq … IHU) /2/
+#U #U2 #_ #HU2 #IHU @(tpss_trans_eq … IHU) /2 width=3/
 qed.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_tpss.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_tpss.ma
index 57e4fb199..fc340e1ad 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_tpss.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_tpss.ma
@@ -20,7 +20,7 @@ include "Basic_2/unfold/tpss_lift.ma".
 (* Advanced properties ******************************************************)
 
 lemma tpss_tps: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ≫* T2 → L ⊢ T1 [d, 1] ≫ T2.
-#L #T1 #T2 #d #H @(tpss_ind … H) -H T2 //
+#L #T1 #T2 #d #H @(tpss_ind … H) -T2 //
 #T #T2 #_ #HT2 #IHT1
 lapply (tps_trans_ge … IHT1 … HT2 ?) //
 qed.
@@ -28,31 +28,31 @@ qed.
 lemma tpss_strip_eq: ∀L,T0,T1,d1,e1. L ⊢ T0 [d1, e1] ≫* T1 →
                      ∀T2,d2,e2. L ⊢ T0 [d2, e2] ≫ T2 →
                      ∃∃T. L ⊢ T1 [d2, e2] ≫ T & L ⊢ T2 [d1, e1] ≫* T.
-/3/ qed.
+/3 width=3/ qed.
 
 lemma tpss_strip_neq: ∀L1,T0,T1,d1,e1. L1 ⊢ T0 [d1, e1] ≫* T1 →
                       ∀L2,T2,d2,e2. L2 ⊢ T0 [d2, e2] ≫ T2 →
                       (d1 + e1 ≤ d2 ∨ d2 + e2 ≤ d1) →
                       ∃∃T. L2 ⊢ T1 [d2, e2] ≫ T & L1 ⊢ T2 [d1, e1] ≫* T.
-/3/ qed.
+/3 width=3/ qed.
 
 lemma tpss_strap1_down: ∀L,T1,T0,d1,e1. L ⊢ T1 [d1, e1] ≫* T0 →
                         ∀T2,d2,e2. L ⊢ T0 [d2, e2] ≫ T2 → d2 + e2 ≤ d1 →
                         ∃∃T. L ⊢ T1 [d2, e2] ≫ T & L ⊢ T [d1, e1] ≫* T2.
-/3/ qed.
+/3 width=3/ qed.
 
 lemma tpss_strap2_down: ∀L,T1,T0,d1,e1. L ⊢ T1 [d1, e1] ≫ T0 →
                         ∀T2,d2,e2. L ⊢ T0 [d2, e2] ≫* T2 → d2 + e2 ≤ d1 →
                         ∃∃T. L ⊢ T1 [d2, e2] ≫* T & L ⊢ T [d1, e1] ≫ T2.
-/3/ qed.
+/3 width=3/ qed.
 
 lemma tpss_split_up: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫* T2 →
                      ∀i. d ≤ i → i ≤ d + e →
                      ∃∃T. L ⊢ T1 [d, i - d] ≫* T & L ⊢ T [i, d + e - i] ≫* T2.
-#L #T1 #T2 #d #e #H #i #Hdi #Hide @(tpss_ind … H) -H T2
-[ /2/
+#L #T1 #T2 #d #e #H #i #Hdi #Hide @(tpss_ind … H) -T2
+[ /2 width=3/
 | #T #T2 #_ #HT12 * #T3 #HT13 #HT3
-  elim (tps_split_up … HT12 … Hdi Hide) -HT12 Hide #T0 #HT0 #HT02
+  elim (tps_split_up … HT12 … Hdi Hide) -HT12 -Hide #T0 #HT0 #HT02
   elim (tpss_strap1_down … HT3 … HT0 ?) -T [2: <plus_minus_m_m_comm // ]
   /3 width=7 by ex2_1_intro, step/ (**) (* just /3 width=7/ is too slow *)
 ]
@@ -64,9 +64,9 @@ lemma tpss_inv_lift1_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 →
                          ∃∃T2. K ⊢ T1 [d, dt + et - (d + e)] ≫* T2 & ↑[d, e] T2 ≡ U2.
 #L #U1 #U2 #dt #et #HU12 #K #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet
 elim (tpss_split_up … HU12 (d + e) ? ?) -HU12 // -Hdedet #U #HU1 #HU2
-lapply (tpss_weak … HU1 d e ? ?) -HU1 // <plus_minus_m_m_comm // -Hddt Hdtde #HU1
-lapply (tpss_inv_lift1_eq … HU1 … HTU1) -HU1 #HU1 destruct -U1;
-elim (tpss_inv_lift1_ge … HU2 … HLK … HTU1 ?) -HU2 HLK HTU1 // <minus_plus_m_m /2/
+lapply (tpss_weak … HU1 d e ? ?) -HU1 // <plus_minus_m_m_comm // -Hddt -Hdtde #HU1
+lapply (tpss_inv_lift1_eq … HU1 … HTU1) -HU1 #HU1 destruct
+elim (tpss_inv_lift1_ge … HU2 … HLK … HTU1 ?) -HU2 -HLK -HTU1 // <minus_plus_m_m /2 width=3/
 qed.
 
 (* Main properties **********************************************************)
@@ -74,20 +74,20 @@ qed.
 theorem tpss_conf_eq: ∀L,T0,T1,d1,e1. L ⊢ T0 [d1, e1] ≫* T1 →
                       ∀T2,d2,e2. L ⊢ T0 [d2, e2] ≫* T2 →
                       ∃∃T. L ⊢ T1 [d2, e2] ≫* T & L ⊢ T2 [d1, e1] ≫* T.
-/3/ qed.
+/3 width=3/ qed.
 
 theorem tpss_conf_neq: ∀L1,T0,T1,d1,e1. L1 ⊢ T0 [d1, e1] ≫* T1 →
                        ∀L2,T2,d2,e2. L2 ⊢ T0 [d2, e2] ≫* T2 →
                        (d1 + e1 ≤ d2 ∨ d2 + e2 ≤ d1) →
                        ∃∃T. L2 ⊢ T1 [d2, e2] ≫* T & L1 ⊢ T2 [d1, e1] ≫* T.
-/3/ qed.
+/3 width=3/ qed.
 
 theorem tpss_trans_eq: ∀L,T1,T,T2,d,e.
                        L ⊢ T1 [d, e] ≫* T → L ⊢ T [d, e] ≫* T2 →
                        L ⊢ T1 [d, e] ≫* T2. 
-/2/ qed.
+/2 width=3/ qed.
 
 theorem tpss_trans_down: ∀L,T1,T0,d1,e1. L ⊢ T1 [d1, e1] ≫* T0 →
                          ∀T2,d2,e2. L ⊢ T0 [d2, e2] ≫* T2 → d2 + e2 ≤ d1 →
                          ∃∃T. L ⊢ T1 [d2, e2] ≫* T & L ⊢ T [d1, e1] ≫* T2.
-/3/ qed.
+/3 width=3/ qed.
-- 
2.39.2