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

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat.ma
index b4aac4eff..7522eb697 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat.ma
@@ -35,7 +35,7 @@ interpretation
   "infinity (non-negative integers with infinity)"
   'Infinity = yinf.
 
-(* Inversion lemmas *********************************************************)
+(* Inversions ***************************************************************)
 
 (* Note: destruct *)
 (*** yinj_inj *)
@@ -43,7 +43,7 @@ lemma eq_inv_yinj_bi (y1) (y2): yinj y1 = yinj y2 → y1 = y2.
 #x #y #H destruct //
 qed-.
 
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
 
 (*** eq_ynat_dec *)
 lemma eq_ynat_dec (y1,y2:ynat): Decidable (y1 = y2).