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>

Add utils to follow the path to an incorrect proof step and to create an error message from invalid proof judgement

Now variables are always shown with a leading ? (except when following a binder)