- support for atomic arities and candidates of reducibility started

[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 c5e93ce16be674a846375d4d484870317f91ecdc..22818a9802bf43b3292d2f6b6421ec4bd3b56403 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 width=1/ | skip ]
+@transitive_le [3: @IHL |2: /2 width=2/ | skip ]
 qed.
 
 (* Basic_1: removed theorems 6: