A semigroup `S` is said to be *with involution* if it comes equipped with an
"inverse-like" operation `rev`. Specifically, the following must hold for all `x
y : S`:
- `rev (rev x) = x`
- `rev (x <> y) = rev y <> rev x.`

`reverse` is the prototypical example. Any group inverse automatically satisfies
these laws.