X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fsubstitution%2Ftps.ma;fp=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fsubstitution%2Ftps.ma;h=9f10dcc2a830c15c52919356a71a311a78452dff;hb=9581b03be2b2bc830820b93992920aaa2c021cc9;hp=744c00b81cf4a291b5ed802763da7107e6a81213;hpb=2983f88c7fedc8973e1104322fa884fb6b3cfb30;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma
index 744c00b81..9f10dcc2a 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma
@@ -220,11 +220,7 @@ lemma tps_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 [d, 0] ≫ T2 → T1 = T2.
 
 lemma tps_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → #[T1] ≤ #[T2].
 #L #T1 #T2 #d #e #H elim H normalize -H L T1 T2 d e
-[ //
-| /2/
-| /3 by monotonic_le_plus_l, le_plus/ (**) (* just /3/ is too slow *)
-| /3 by monotonic_le_plus_l, le_plus/ (**) (* just /3/ is too slow *)
-] 
+/3 by monotonic_le_plus_l, le_plus/ (**) (* just /3/ is too slow *)
 qed-.
 
 (* Basic_1: removed theorems 25: