While using the general rewriting for some complex statement, I realized that the following (distilled version) does not work:

```
From Coq Require Import Morphisms Morphisms_Relations Relation_Definitions RelationClasses.
Inductive my_ty : Set :=
| my_ty_cons : my_ty
.
Notation "R <~> R'" := (@relation_equivalence my_ty R R') (at level 90, no associativity).
Inductive my_rel : relation my_ty :=
| my_rel_cons : my_rel my_ty_cons my_ty_cons
.
Set Debug "tactic-unification".
Goal forall a b Rgen (x : nat),
Rgen x <~> my_rel ->
Rgen x a b ->
my_rel a b.
Proof.
Search relation_equivalence.
intros * H H0.
Fail setoid_rewrite H in H0.
change (Rgen x) with (fun a b => Rgen x a b) in H0.
Fail setoid_rewrite H in H0.
Abort.
Context (pr : subrelation relation_equivalence (pointwise_relation my_ty (pointwise_relation my_ty iff))).
Goal forall a b Rgen (x : nat),
Rgen x <~> my_rel ->
Rgen x a b ->
my_rel a b.
Proof.
Search relation_equivalence.
intros * H H0.
change (Rgen x) with (fun a b => Rgen x a b) in H0.
setoid_rewrite H in H0.
Abort.
```

In the first goal, both rewriting fails, specifically the first one fails because of unification failure. Why does it unify `Rgen x`

(the left side of `<~>`

) only with `Rgen x a b`

, `Rgen`

, `x`

, `a`

, `b`

, but never with `Rgen x`

?

This works once I use `change (Rgen x) with (fun a b => Rgen x a b) in H0.`

(so that `(fun a b => Rgen x a b)`

becomes a head by itself), but then the problem is about that `subrelation`

I put as a `Context`

. Why does this rewriting requires that? Isnâ€™t the `Proper`

instance for `relation_equivalence`

not enough?