update in ground

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

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat.ma
index b4aac4eff753341a1dfa8b702cebf4ca96b1b632..7522eb6971c8a1d26f3ada54712c01e3e7f5f73e 100644 (file)
--- 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).