Update STYLE, incorporating wiki; close #468

Oh, maybe I remember: if `^-1` means `equiv_inverse`, then `f^-1 (f x)` is not syntactically identical to the LHS of `eissect`, and I think I remember that causing problems.  Perhaps that would not be a problem any more with keyed unification?