]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma
rtmap (platform-indepent multple relocation): application and composition
[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / ynat / ynat_succ.ma
index be5bef7077887a884a6bab177c010fe523e28ea1..f08e632937ee67dd06dfb6bac7392125d1ce9389 100644 (file)
@@ -12,7 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground_2/notation/functions/successor_1.ma".
 include "ground_2/ynat/ynat_pred.ma".
 
 (* NATURAL NUMBERS WITH INFINITY ********************************************)