* When an unexpected token is encountered, add the string representation of the token
to the exception
* When printing of a sequent / formula / term fails, try to identify the smallest structure
on which the printing fails by attempting to print all subformulas and subterms. Report that
printing failed on the smallest structure rather than on the whole sequent / formula / term.

Represented as And() and Or() respectively.

Simply print the formula and expect it to be equal to the string
instead of parsing the string and expecting it to be equal to the
formula. Not all tests of the parser are tests for printer, because
there exist multiple strings that correspond to the same formula
(due to extra parentheses and multiple ways to write connectors).

* equality does not have to be parenthesized
* 'and' has higher priority than 'or', so parentheses are not needed to express order
* '∀ ?x.' instead of '∀x.'

Add inverse functions for all parsing rules. Further simplify parsing
of binder formulas and factor out toplevel (iff, implies) connector
formulas to make printing implementation easier.

Add tests for sequent parsing.

Implement a parser for first order logic with equality and schematic functions/predicates
using scallion.

Require that PredicateFormula's and ConnectorFormula's args correspond to the label's arity

General grammatical updates for reference manual

PeanoArithmetics contains the definitions and axioms of Peano arithmetics,
PeanoArithmeticsLibrary gives access to lisa.utils.Library with runningPeanoTheory,
Peano contains proofs of the theory. This separation follows the same structure
as set theory.

Analogous to the existing requirement in FunctionTerm.

Fix a broken link to the reference manual

Signed-off-by: Sankalp Gambhir <sankalp.gambhir47@gmail.com>