summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/shouldsucceed/1905.v
blob: bd7fd79672b4b6cca967dcc09d63f734d2f039b2 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13

Require Import Setoid.

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.