Strange failure of general rewriting

Using Coq
1

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?