- lambda_delta: context-free weak head normal forms continued ...

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / substitution / tps.ma

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 744c00b81cf4a291b5ed802763da7107e6a81213..9f10dcc2a830c15c52919356a71a311a78452dff 100644 (file)
--- 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: