X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fynat_pred_succ.ma;h=065f8e8af7426b4c2abda8a1d5f76d4ef30fcf50;hb=4d232392091ee233afc26ecf3120dd5f5c6a33c8;hp=b03fe0d595a965521ce5033874a4f15978b4126e;hpb=da0775e27b362e91ea1453a800bc403781cc2ca3;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_pred_succ.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_pred_succ.ma
index b03fe0d59..065f8e8af 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_pred_succ.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_pred_succ.ma
@@ -25,7 +25,7 @@ lemma ypred_succ (x): x = ↓↑x.
 #x @(ynat_split_nat_inf … x) -x //
 qed.
 
-(* Inversion with ysucc *****************************************************)
+(* Inversions with ysucc ****************************************************)
 
 (*** ynat_cases *)
 lemma ynat_split_zero_pos (x): ∨∨ 𝟎 = x | x = ↑↓x.