Extensional setoids on functions, and rewriting

[Blaisorblade]

For everybody involved (including @gmalecha), @Yannick found a useful fix, and even by looking (and trusting!) the error messages from Coq’s rewrite:

Confused with a failure of a generalized rewrite

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 co…

For more examples, see:

Fix setoid rewriting for function application in Iris (#312) · Issues · Iris...