Generalized rewriting support for "respectful_hetero"

Description of the problem

Hi, I'd like to use rewrite with respectful_hetero. See following code:

Require Import Morphisms Setoid RelationClasses.

Section test1.

  Context (A B : Type) (R : relation A) (S : A -> relation B) (perR: PER R) (perS: forall a, PER (S a))
          (f : A -> B) (proper_f: Proper (@respectful_hetero A A (fun _ => B) (fun _ => B) R (fun a _ => (S a))) f)
          (x y : A) (pf: R x y).

  (* This works *)
  Goal S x (f y) (f y) -> S x (f x) (f y).
  intros.
  (* This doesn't work: *) Fail setoid_rewrite pf.
  (* But the proof can still be completed easily. *) apply proper_f. exact pf. Defined.

End test1.

Section test2. (* This shows why I would want to do this. *)

  Context (A B C : Type) (R : relation A) (S : A -> relation B) (T : relation C) (P : A -> Prop) (perR: PER R) (perS: forall a:A, PER (S a)) (perT: PER T)
          (f : A -> B -> C) (proper_S : Proper (R ==> relation_equivalence) S) (proper_f: Proper (@respectful_hetero A A (fun _ => B -> C) (fun _ => B -> C)
            R (fun a a' => (respectful (S a) T))) f)
          (a a' : A) (pfa : R a a') (b b' : B) (pfb : S a b b').

  Goal T (f a' b') (f a' b') -> T (f a b) (f a' b').
  intros.
  (* This doesn't work: *) Fail rewrite pfa.
  (* This doesn't work either: *) Fail rewrite pfb.
  (* But the proof can still be completed easily. *) apply proper_f. exact pfa. exact pfb. Defined.  

End test2.

I see some Ltac code mentioning rewrite and respectful_hetero in the "genreweqwip" branch of @mattam82's fork: https://github.com/search?q=repo%3Amattam82%2Fcoq%20respectful_hetero&type=code Is this relevant?

Coq Version

I am running The Coq Proof Assistant, version 8.16.1, compiled with OCaml 4.13.1.

Start by running the two Coq reproductions in the issue and inspect the existing rewrite handling for respectful_hetero; the report mentions Ltac code in the "genreweqwip" branch as a possible reference. Done means rewrite or setoid_rewrite handles the shown test1 and test2 cases, with corresponding regression coverage.