Not an etymological post, as I was first expecting, but a post on the use of rewrite tactics in Coq using something other than equality, based on Partial Equiva

Not an etymological post, as I was first expecting, but a post on the use of rewrite tactics in Coq using something other than equality, based on Partial Equivalence Relations (PER) and their proper elements (those that are related to themselves—which would be everything for honest equivalence relations, but partial equivalence relations drop that requirement).