LP facilitates matching terms involving associative-commutative (ac) operators by using a special

When an argument of an ac operator has that operator as its principal operator,
LP replaces it by its arguments. For example, when `+` is ac,
`(a + b) + (c + d)` flattens to `a + b + c + d`.

Furthermore, when a flattened term involving an ac operator has more than two
arguments, LP sorts the arguments lexicographically; for example, when `+` is
ac, `(c + b) + a` flattens to `a + b + c`.

Two-argument terms such as `q <=> p`, where `<=>` is the hardwired ac
operator for boolean equivalence, are not flattened to `p <=> q`. This
enables LP to orient them into rewrite rules in the
direction the user (may have) intended.