where 
and 
.
Inversion lemmas in the library must be named opid-of-r
_inversion.
Inversion lemmas are required for equivalence relations, but not equality or order relations. They are used by the Rev* atomic conversions, and in conjunction with the weakening, transitivity, and functionality lemmas when these lemmas mix order and equivalence relations.