X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fgrammar%2Fcl_weight.ma;h=c5e93ce16be674a846375d4d484870317f91ecdc;hb=04cd2181640b3828b3d193a8e819c849ef574236;hp=0414499a59de0aee49a610b8bf83394a6388d970;hpb=fc7af5f9ea2cd4a876b8babc6b691136799e3c87;p=helm.git

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 0414499a5..c5e93ce16 100644
--- 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: