test-suite/bugs/closed/1905.v


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.