Hi @Blaisorblade ,
Thanks a lot for your answer!
However, as much as this connex question is also very much of interest to me as well, I do not believe it to be directly related to this issue at hand.
The instance eq_rel_rewrite does allow extensional rewriting in this context, which actually is what happens in the first Goal (I rewrite R ≡ S in the goal R x y by virtue of the pointwise_relation part of the instance).
The failure is the exact same case, but instantiated with slightly more complex “R” and “S”. The equation F († R) ≡ † (F R) is already in my context, I do not need to derive it.
Best,
Yannick