]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/nlibrary/datatypes/list.ma
update in groud_2 and models
[helm.git] / helm / software / matita / nlibrary / datatypes / list.ma
index 87f91718526c1384736c4015e4f42e535a9f7acc..836b72ea5bbebe046d2d3825015bc8822361c62f 100644 (file)
@@ -13,7 +13,6 @@
 (**************************************************************************)
 
 include "logic/pts.ma".
-include "logic/equality.ma".
 include "arithmetics/nat.ma".
 
 ninductive list (A:Type[0]) : Type[0] ≝