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)

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.

Changed final class into sealed class for scala2 compiler

FUlly reorganised theory files. All seems functionning. Theory files now all simply have to extend proven.Main, and get every import and tool.
Documentation for recent development.
Adaptation of existing Set Theory proofs to the new canonical style.

Printing, constructing theorems and all kinds of definitions, authomatic conversions, and much more.

Printer file moved to utilities
New organisation of helpers, new helper file for RunningTheory and their elements. Can show Justifications
SCProofCheckerJudgement now contain the proof they refer to, no need to pass it explicitely along anymore.
Other small changes.

This commit introduces the separation between Function/Predicate labels and
theory symbols. Both constant and schematic function labels behave as functions,
both constant and schematic predicate labels behave as predicates, but only
constant function and predicate labels can be symbols in a theory. This is now
expressed in the project by a marker trait TheorySymbol.

Added scalafmt, scalafix and github ci as suggested in https://github.com/epfl-lara/lisa/pull/4/files.
Code reformated.

Corrected a bug in the equivalence checker. Due to small optimisations, part of checkForContradiction was reversing a list at one point, and expecting it not reverse at some other point.
This made the check non-sufficient.

Correction of small error regarding function and predicate definition. Fix to missing case in printer match.