update in ground

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

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 b03fe0d595a965521ce5033874a4f15978b4126e..065f8e8af7426b4c2abda8a1d5f76d4ef30fcf50 100644 (file)
--- 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.