- "grammar" component updated to new syntax ...

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / grammar / cl_weight.ma

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma
index 0414499a59de0aee49a610b8bf83394a6388d970..c5e93ce16be674a846375d4d484870317f91ecdc 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma
@@ -38,7 +38,7 @@ qed.
 lemma tw_shift: ∀L,T. #[L, T] ≤ #[L @ T].
 #L elim L //
 #K #I #V #IHL #T
-@transitive_le [3: @IHL |2: /2/ | skip ]
+@transitive_le [3: @IHL |2: /2 width=1/ | skip ]
 qed.
 
 (* Basic_1: removed theorems 6: