From cb7f8dd59d9b6d60671b634156ca410c737ff218 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 30 Dec 2009 17:31:18 +0000 Subject: [PATCH] Removed line is back again. --- helm/software/matita/nlibrary/nat/nat.ma | 1 + 1 file changed, 1 insertion(+) diff --git a/helm/software/matita/nlibrary/nat/nat.ma b/helm/software/matita/nlibrary/nat/nat.ma index eed1efd1c..e9d32973b 100644 --- a/helm/software/matita/nlibrary/nat/nat.ma +++ b/helm/software/matita/nlibrary/nat/nat.ma @@ -14,6 +14,7 @@ include "hints_declaration.ma". include "logic/equality.ma". +include "sets/setoids.ma". ninductive nat: Type[0] ≝ O: nat -- 2.39.2