summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/shouldsucceed/1905.v
blob: 8c81d7510b0ac50f41651a80f1eb2cca61450a8d (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.