blob: 92a7c6ccbc4149c67532a83e0cbc2693bff4e1b2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
|
(* Some tests for contradiction *)
Lemma L1 : forall A B : Prop, A -> ~A -> B.
Proof.
intros; contradiction.
Qed.
Lemma L2 : forall A B : Prop, ~A -> A -> B.
Proof.
intros; contradiction.
Qed.
Lemma L3 : forall A : Prop, ~True -> A.
Proof.
intros; contradiction.
Qed.
Lemma L4 : forall A : Prop, forall x : nat, ~x=x -> A.
Proof.
intros; contradiction.
Qed.
Lemma L5 : forall A : Prop, forall x y : nat, ~x=y -> x=y -> A.
Proof.
intros; contradiction.
Qed.
Lemma L6 : forall A : Prop, forall x y : nat, x=y -> ~x=y -> A.
Proof.
intros; contradiction.
Qed.
|
