X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fdatatypes%2Flist.ma;h=836b72ea5bbebe046d2d3825015bc8822361c62f;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=87f91718526c1384736c4015e4f42e535a9f7acc;hpb=1d7773584ddd6463b0941026f114b0173e3b6b72;p=helm.git

diff --git a/helm/software/matita/nlibrary/datatypes/list.ma b/helm/software/matita/nlibrary/datatypes/list.ma
index 87f917185..836b72ea5 100644
--- a/helm/software/matita/nlibrary/datatypes/list.ma
+++ b/helm/software/matita/nlibrary/datatypes/list.ma
@@ -13,7 +13,6 @@
 (**************************************************************************)
 
 include "logic/pts.ma".
-include "logic/equality.ma".
 include "arithmetics/nat.ma".
 
 ninductive list (A:Type[0]) : Type[0] ≝