milestone update in ground_2 and basic_2A

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / ynat / ynat_plus.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma
index 2e1d05077a37e9fd25e5d328ba893097629c97e9..9e0db4161dde3a7e6786d20a0e8404611ebe4951 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma
@@ -47,7 +47,7 @@ qed.
 lemma yplus_succ_swap: ∀m,n. m + ↑n = ↑m + n.
 // qed.
 
-lemma yplus_SO2: ∀m. m + 1 = ↑m.
+lemma yplus_SO2: ∀m:ynat. m + 1 = ↑m.
 * //
 qed.