From c99cecf223de21ed2ebb32106d661ce8b4dac9a8 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 22 Nov 2006 15:24:20 +0000
Subject: [PATCH 1/1] removed the impredicativity of falsum

---
 helm/software/matita/contribs/RELATIONAL/NLE/fwd.ma   | 6 +++---
 helm/software/matita/contribs/RELATIONAL/NPlus/fwd.ma | 6 +++---
 helm/software/matita/contribs/RELATIONAL/Nat/fwd.ma   | 4 ++--
 3 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/helm/software/matita/contribs/RELATIONAL/NLE/fwd.ma b/helm/software/matita/contribs/RELATIONAL/NLE/fwd.ma
index f61fadfee..5ddeb41af 100644
--- a/helm/software/matita/contribs/RELATIONAL/NLE/fwd.ma
+++ b/helm/software/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/helm/software/matita/contribs/RELATIONAL/NPlus/fwd.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/fwd.ma
index 0b8ba2b88..7aea3af9d 100644
--- a/helm/software/matita/contribs/RELATIONAL/NPlus/fwd.ma
+++ b/helm/software/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/helm/software/matita/contribs/RELATIONAL/Nat/fwd.ma b/helm/software/matita/contribs/RELATIONAL/Nat/fwd.ma
index 0938e4d9a..b76138fe5 100644
--- a/helm/software/matita/contribs/RELATIONAL/Nat/fwd.ma
+++ b/helm/software/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.
 
-- 
2.39.2