test-suite/bugs/closed/bug_3257.v


1
2
3
4
5
6

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