update in ground

[helm.git] / matita / matita / contribs / lambdadelta / ground / arith / ynat_plus.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_plus.ma
index 61dd0b4b1752b85f19fe000527f2580d5a19868b..f76cbc115bb118588de873b61010498f0680be55 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_plus.ma
@@ -78,7 +78,7 @@ lemma yplus_inj_bi (n) (m):
 <nplus_succ_dx >ysucc_inj >ysucc_inj <yplus_succ_dx //
 qed.
 
-(* Advaced constructions ****************************************************)
+(* Advanced constructions ***************************************************)
 
 (*** ysucc_iter_Y yplus_Y1 *)
 lemma yplus_inf_sn (x): ∞ = ∞ + x.