blob: 9831a4d205d9f900379dd9898a4952294b37b9fe (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
Inductive even: nat -> Prop :=
| evenB: even 0
| evenS: forall n, even n -> even (S (S n)).
Goal even 1 -> False.
Proof.
refine (fun a => match a with end).
Qed.
Goal even 1 -> False.
Proof.
refine (fun a => match a in even n
return match n with 1 => False | _ => True end : Prop
with evenB => I | evenS _ _ => I end).
Qed.
|
