From 4fa0b4742e97c973000c9b9b48523c0a22531b91 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 11 Jul 2006 17:08:41 +0000 Subject: [PATCH] dependences updated again :) --- .../software/matita/contribs/RELATIONAL-ARITHMETICS/nat_defs.ma | 2 ++ helm/software/matita/contribs/RELATIONAL-ARITHMETICS/nat_fwd.ma | 1 - 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/nat_defs.ma b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/nat_defs.ma index 9b8ab4571..30d6cfb5c 100644 --- a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/nat_defs.ma +++ b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/nat_defs.ma @@ -14,6 +14,8 @@ set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/nat_defs". +include "logic/equality.ma". + inductive nat: Set \def | O: nat | S: nat \to nat. diff --git a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/nat_fwd.ma b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/nat_fwd.ma index bfab390fd..952a8cbf0 100644 --- a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/nat_fwd.ma +++ b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/nat_fwd.ma @@ -14,7 +14,6 @@ set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/nat_fwd". -include "logic/equality.ma". include "nat_defs.ma". theorem eq_gen_O_S: \forall (P:Prop). \forall m2. O = S m2 \to P. -- 2.39.2