X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Fynat%2Fynat_plus.ma;h=9e0db4161dde3a7e6786d20a0e8404611ebe4951;hp=2e1d05077a37e9fd25e5d328ba893097629c97e9;hb=1fd63df4c77f5c24024769432ea8492748b4ac79;hpb=277fc8ff21ce3dbd6893b1994c55cf5c06a98355

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 2e1d05077..9e0db4161 100644
--- 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.