[mezpusz]

This PR fixes most of the errors that GDV reported due to mostly not properly parenthesized higher-order or FOOL terms. It also removes a bunch of unneeded parenthesization. The idea is that we pass down a flag whether the outer context requires the inner context to parenthesize itself. The main guidelines are the following:

1. for formulas, we do not parenthesize atomic things, such as predicates, names, $true, $false, etc.
2. we only parenthesize negation and quantifiers when the outer context requires it (for example when a term contains the formula)
3. we parenthesize binary Boolean operators when they are not on the top-level (either subterm or subformula)
4. equations are tricky and I don't know how they fit into the Boolean symbol precedences, so we parenthesize their sides by the above rules
5. normal term or literal arguments or quantifier lists do not need parenthesization, as commas and outer parentheses guard them
6. lambdas and applications we parenthesize when they are not top-level (either subterm or subformula)
7. proxy symbols need parentheses even when they are just by themselves, unapplied

See examples in testing code, we can discuss if something looks fishy.

There might be some places, like literals in clauses, where we had parentheses before and might need them again but GDV hasn't complained so far.

I also sneaked in a few smaller fixes for GDV, (1) using underscores for non-alphanumeric characters in inference names, and (2) fixing two-variable-equality sort recognition for literals in clauses.

There are a few small errors that still need fixing, mostly related to finding the right fragment we are in and wrong order of quantified variables.

[MichaelRawson]

Cool! Guess you didn't need a precedence enumeration, only Boolean yes/no parens in the end?

[mezpusz]

Cool! Guess you didn't need a precedence enumeration, only Boolean yes/no parens in the end?

Yes, turns out the precedences were set in the right way already for formulas, we just had some problems between term-formula boundaries.