From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 22 Nov 2006 15:24:20 +0000 (+0000)
Subject: removed the impredicativity of falsum
X-Git-Tag: 0.4.95@7852~798
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7bd959df2e265883f1c8b698529909dd0078a558;p=helm.git

removed the impredicativity of falsum
---

diff --git a/matita/contribs/RELATIONAL/NLE/fwd.ma b/matita/contribs/RELATIONAL/NLE/fwd.ma
index f61fadfee..5ddeb41af 100644
--- a/matita/contribs/RELATIONAL/NLE/fwd.ma
+++ b/matita/contribs/RELATIONAL/NLE/fwd.ma
@@ -36,16 +36,16 @@ theorem nle_gen_succ_succ: \forall x,y. x < succ y \to x <= y.
  auto.
 qed.
 
-theorem nle_gen_succ_zero: \forall (P:Prop). \forall x. x < zero \to P.
+theorem nle_gen_succ_zero: \forall x. x < zero \to False.
  intros.
  lapply linear nle_gen_succ_1 to H. decompose.
- apply (eq_gen_zero_succ ? ? H1).
+ lapply linear eq_gen_zero_succ to H1. decompose.
 qed.
 
 theorem nle_gen_zero_2: \forall x. x <= zero \to x = zero.
  intros 1. elim x; clear x; intros;
  [ auto new timeout=30
- | apply (nle_gen_succ_zero ? ? H1)
+ | lapply linear nle_gen_succ_zero to H1. decompose.
  ].
 qed.
 
diff --git a/matita/contribs/RELATIONAL/NPlus/fwd.ma b/matita/contribs/RELATIONAL/NPlus/fwd.ma
index 0b8ba2b88..7aea3af9d 100644
--- a/matita/contribs/RELATIONAL/NPlus/fwd.ma
+++ b/matita/contribs/RELATIONAL/NPlus/fwd.ma
@@ -40,14 +40,14 @@ theorem nplus_gen_zero_2: \forall p,r. (p + zero == r) \to p = r.
  intros. inversion H; clear H; intros;
  [ auto new timeout=30
  | clear H H1.
-   lapply eq_gen_zero_succ to H2 as H0. apply H0
+   lapply eq_gen_zero_succ to H2 as H0. decompose.
  ].
 qed.
 
 theorem nplus_gen_succ_2: \forall p,q,r. (p + (succ q) == r) \to 
                           \exists s. r = (succ s) \land p + q == s.
  intros. inversion H; clear H; intros;
- [ lapply eq_gen_succ_zero to H as H0. apply H0
+ [ lapply eq_gen_succ_zero to H as H0. decompose.
  | clear H1 H3 r.
    lapply linear eq_gen_succ_succ to H2 as H0.
    subst.
@@ -60,7 +60,7 @@ theorem nplus_gen_zero_3: \forall p,q. (p + q == zero) \to
  intros. inversion H; clear H; intros;
  [ subst. auto new timeout=30
  | clear H H1.
-   lapply eq_gen_zero_succ to H3 as H0. apply H0
+   lapply eq_gen_zero_succ to H3 as H0. decompose.
  ].
 qed.
 
diff --git a/matita/contribs/RELATIONAL/Nat/fwd.ma b/matita/contribs/RELATIONAL/Nat/fwd.ma
index 0938e4d9a..b76138fe5 100644
--- a/matita/contribs/RELATIONAL/Nat/fwd.ma
+++ b/matita/contribs/RELATIONAL/Nat/fwd.ma
@@ -18,11 +18,11 @@ include "logic/equality.ma".
 
 include "Nat/defs.ma".
 
-theorem eq_gen_zero_succ: \forall (P:Prop). \forall m2. zero = succ m2 \to P.
+theorem eq_gen_zero_succ: \forall m2. zero = succ m2 \to False.
  intros. destruct H.
 qed.
 
-theorem eq_gen_succ_zero: \forall (P:Prop). \forall m1. succ m1 = zero \to P.
+theorem eq_gen_succ_zero: \forall m1. succ m1 = zero \to False.
  intros. destruct H.
 qed.