Add a generic mechanism for rewriting with any equality satisfying J#21098

tabareau wants to merge 4 commits intorocq-prover:masterrocq-prover/rocq:masterfrom

tabareau:sortpoly-equalitytabareau/rocq:sortpoly-equalityCopy head branch name to clipboard