continuing on lazy pointwise extensions ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / grammar / cl_weight.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma
index aa20d64db45300fba99e5c01762adbf50f8d8bce..d7c923dd494274a4e539b21477579c2df841083d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma
@@ -39,7 +39,7 @@ normalize in ⊢ (?→?→?→?→?→?%%); //
 qed.
 
 lemma fw_lpair_sn: ∀I,G,L,V,T. ♯{G, L, V} < ♯{G, L.ⓑ{I}V, T}.
-normalize /3 width=1 by monotonic_lt_plus_l, monotonic_le_plus_r/ (**) (* auto too slow without trace *)
+normalize /3 width=1 by monotonic_lt_plus_l, monotonic_le_plus_r/
 qed.
 
 (* Basic_1: removed theorems 7: