test-suite/bugs/closed/3257.v


1
2
3
4
5

Require Import Setoid Morphisms Basics.
Lemma foo A B (P : B -> Prop) :
  pointwise_relation _ impl (fun z => A -> P z) P.
Proof.
  Fail reflexivity.