* 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.

Analogous to the existing requirement in FunctionTerm.

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)

Any work on top of current LISA release should be easily adaptable by:
 - Changing all instances of Arity 0 SchematicFunctionLabel by VariableLabel
 - Changing all instances of Arity 0 SchematicPredicateLabel by VariableFormulaLabel
 - Changing all matching on SchematicFunctionLabel by either VariableLabel, SchematicFunctionLabel or SchematicTermLabel, according to whether the arity should be =0, >0 or >=0.
 - Changing all instances of multiary SchematicPredicateLabel by SchematicNPredicateLabel
 - Removing the empty parenthesis () that where used to transform an Arity 0 label to a term or formula. Variables have the implicit conversion without the call.

Changed the whole project to remove 0-arity schematic variables and replace them by variables. It compiles, but at least one proof doesn't go through.