X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FRELATIONAL-ARITHMETICS%2Fnat_defs.ma;h=a78886780fa09cb9f2b4f251110f166f4fa1dd98;hb=ac8bbbb47941fdf5b2d602b1e2ab2a6d6dcec9cd;hp=a188208f2f76c69c35c6d2fde0b3a4c02e2c5918;hpb=389b29d17694ba6abe79dfd36d862321e05d17d6;p=helm.git

diff --git a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/nat_defs.ma b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/nat_defs.ma
index a188208f2..a78886780 100644
--- a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/nat_defs.ma
+++ b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/nat_defs.ma
@@ -19,7 +19,3 @@ include "library/logic/equality.ma".
 inductive nat: Set \def
    | O: nat
    | S: nat \to nat.
-
-theorem eq_gen_O_S: \forall (P:Prop). \forall m2. O = S m2 \to P.
- intros. inversion H.
-