blob: 0f573a2898003714897ea380dee6617069516b63 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
(* Tauto bug initially due to wrong test for binary connective *)
Parameter A B : Type.
Axiom P : A -> B -> Prop.
Inductive IP (a : A) (b: B) : Prop :=
| IP_def : P a b -> IP a b.
Goal forall (a : A) (b : B), IP a b -> ~ IP a b -> False.
Proof.
intros.
tauto.
Qed.
|
