removed the impredicativity of falsum

diff --git a/matita/contribs/RELATIONAL/NLE/fwd.ma b/matita/contribs/RELATIONAL/NLE/fwd.ma
index f61fadfeee5f2b42b24b73aeca5b037c1e6af0be..5ddeb41aff1b1efe28b47c639310f49cd8373f50 100644 (file)
--- 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 0b8ba2b889b35456329db195600137dee4dbed4d..7aea3af9d785e13fa3ff87d09f0348a838efdbd6 100644 (file)
--- 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 0938e4d9ab470234b5d420134410b9c76c244e86..b76138fe56998d8055c97dac00e36c88318b7ce8 100644 (file)
--- 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.