]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/ground/arith/nat_succ_iter.ma
arithmetics for λδ
[helm.git] / matita / matita / contribs / lambdadelta / ground / arith / nat_succ_iter.ma
index 640e84d6de811ccc7af314610e8414711e8150ca..b3eee20682dded54198b27b5036c1a0d1003f12d 100644 (file)
@@ -15,7 +15,7 @@
 include "ground/arith/nat_iter.ma".
 include "ground/arith/nat_succ.ma".
 
-(* NON-NEGATIVE INTEGERS ****************************************************)
+(* SUCCESSOR FOR NON-NEGATIVE INTEGERS **************************************)
 
 (* Rewrites with niter ******************************************************)