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

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt.ma
index a76ccd946..e9531df33 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt.ma
@@ -29,7 +29,7 @@ interpretation
 
 (* Basic destructions *******************************************************)
 
-(* ylt_fwd_gen ylt_inv_Y2 *)
+(*** ylt_fwd_gen ylt_inv_Y2 *)
 lemma ylt_des_gen_sn (x) (y):
       x < y → ∃m. x = yinj_nat m.
 #x #y * -x -y