Convert formulas to OLP commands in set-theory

Material from Tim Button in the set-theory part contains formulas. These have formulas hardcoded as \phi instead of !A etc, use \exists and \forall instead of \lexists and \lforall, don't use \eq for identity, and in some cases have atomic formulas without parentheses around arguments. To fix this, will need ability of \lforall and \lexists to have guards, e.g., \lforall(x \in \alpha)[!A(x)] should produce (\forall x \in \alpha), !A(x).

Start by locating the set-theory material and the definitions or uses of \lforall and \lexists. Review the formula conventions described in the issue, including !A, guarded quantifiers, \eq for identity, and parenthesized atomic arguments; the work is done when the material follows those conventions and guarded commands produce the stated output.