Dear Coq users,

I have a parametric relation `myeq`

that I would like to rewrite under the predicate `P`

whenever both are used with the same parameter. It works well if I declare the appropriate morphism:

```
From Coq Require Import Setoid Morphisms.
Parameter A B : Type.
Parameter myeq : A -> relation B.
Add Parametric Relation (a : A) : B (myeq a) as myeq_rel.
Parameter P : A -> B -> Prop.
Add Parametric Morphism (a : A) : (P a)
with signature (myeq a) ==> iff as P_morphism.
Admitted.
Lemma test1 b1 b2 :
(forall a, myeq a b1 b2) ->
exists a, P a b1.
Proof.
intro.
setoid_rewrite H. (* OK *)
Abort.
```

However it stops working when I try to apply a function, even registered as a morphism for `myeq`

:

```
Parameter Op : B -> B.
Add Parametric Morphism (a : A) : Op
with signature (myeq a) ==> (myeq a) as op_morphism.
Admitted.
Lemma test2 b1 b2 :
(forall a, myeq a b1 b2) ->
exists a, P a (Op b1).
Proof.
intro.
setoid_rewrite H. (* not OK, why? *)
Abort.
```

Typeclasses debug information mention some early unification failure, but it leaves me puzzled.

Did I forget to declare something?