X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Funfold%2Fltpss_ldrop.ma;h=c9a8dda93b129f344c428d284fe553f9cb55fe56;hb=7aa41e02e64bd09df253cc4267a44b4f49b16e03;hp=14d529db8ebee5a86a09f25c7be412976acb5fe5;hpb=d38087520d6ce1d696b28da40f3811291fc8a311;p=helm.git

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.