Types

Created by: SimonGuilloud

This PR is about making a front end for first order logic, allowing to define more specialized Terms, starting with functions, numbers and pairs and ultimately arbitrary types. The implementation aims to be as general as possible to allow for future development. Incidentally, it solves some unsatisfactory problems of using the Kernel's FOL: The difference between Variables and VariableLabels, runtime assertions to check arity (with the updated "front" this is checked at compile time), etc.

With FOL redefined, it needs to be integrated to the existing proof framework, while maintaining correspondance with kernel objects. Depending of the kind of object, this range from easy to systematic but tedious to non-trivial.