X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fnat_pred_succ.ma;h=3d79e371ebb0561e12510868a5af77df236c3868;hp=b7f9918b08d0191cf52391c310700d278be31116;hb=4d232392091ee233afc26ecf3120dd5f5c6a33c8;hpb=da0775e27b362e91ea1453a800bc403781cc2ca3

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_pred_succ.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_pred_succ.ma
index b7f9918b0..3d79e371e 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_pred_succ.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_pred_succ.ma
@@ -24,7 +24,7 @@ lemma npred_succ (n): n = ↓↑n.
 * //
 qed.
 
-(* Inversion with nsucc *****************************************************)
+(* Inversions with nsucc ****************************************************)
 
 (*** nat_split *)
 lemma nat_split_zero_pos (n): ∨∨ 𝟎 = n | n = ↑↓n.