blob: 3b8a3d2f681e4b80d1706bbf0590e9b5613f6250 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
Require Import Setoid Program.
Axiom t : Set.
Axiom In : nat -> t -> Prop.
Axiom InE : forall (x : nat) (s:t), impl (In x s) True.
Goal forall a s,
In a s -> False.
Proof.
intros a s Ia.
rewrite InE in Ia.
Admitted.
|