\doc{Proofs of operator theories}
\ref{proof-of-operator-theory}

LP permits users to prove \llink{operator-theory}{operator theories} as well as
\clink{assert} them.  Proving that an operator \f{+} is commutative involves
proving a single subgoal consisting of the formula \fq{x + y = y + x}.  Proving
that an operator is associative-commutative involves proving an additional
subgoal consisting of the formula \fq{x + (y + z) = (x + y) + z}.