X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fynat_plus.ma;h=f76cbc115bb118588de873b61010498f0680be55;hb=4d232392091ee233afc26ecf3120dd5f5c6a33c8;hp=61dd0b4b1752b85f19fe000527f2580d5a19868b;hpb=888840f6b3a71d3d686b53b702d362ab90ab0038;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_plus.ma
index 61dd0b4b1..f76cbc115 100644
--- 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.