# Parametric rewriting under binders

**URL:** https://discourse.rocq-prover.org/t/parametric-rewriting-under-binders/1226
**Category:** Using Rocq
**Created:** [March 3, 2021, 3:52pm UTC](https://discourse.rocq-prover.org/t/parametric-rewriting-under-binders/1226 "2021-03-03T15:52:49Z")
**Posts on this page:** 1
**Page:** 1

<div class="post-metadata">

### Author: ![pjm](https://avatars.discourse-cdn.com/v4/letter/p/c6cbf5/32.png) [@pjm](https://discourse.rocq-prover.org/u/pjm)
#### Post date: [March 3, 2021, 3:52pm UTC](https://discourse.rocq-prover.org/t/parametric-rewriting-under-binders/1226/1 "2021-03-03T15:52:49Z")

</div>

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:

```auto
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` :

```auto
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?