some corrections ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / reduction / cnx.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma
index 9954e6edbc2795eff61fc78bd5b29fba62de7654..d423f119ea1c07d887bb6e69bd8f8e2f91bfade5 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma
@@ -103,7 +103,7 @@ qed.
 
 lemma cnx_sort_iter: ∀h,g,G,L,k,l. deg h g k l → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃⋆((next h)^l k)⦄.
 #h #g #G #L #k #l #Hkl
-lapply (deg_iter … l Hkl) -Hkl <minus_n_n /2 width=1 by cnx_sort/
+lapply (deg_iter … l Hkl) -Hkl <minus_n_n /2 width=6 by cnx_sort/
 qed.
 
 lemma cnx_abst: ∀h,g,a,G,L,W,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃W⦄ → ⦃G, L.ⓛW⦄ ⊢ 𝐍[h, g]⦃T⦄ →