New substitution mechanism

Created by: SimonGuilloud

• "Function like"-terms and formulas, now have a specific syntax.
• The arguments of those functions are now nullary schemas rather than variables
• RightSubstEq, LeftSubstEq, RightSubstIff and LeftSubstIff now accepts arbitrarily many pairs of terms or formulas, i.e. they can do simultaneous substitutions of many pairs of terms or formulas
• InstFunSchema and InstPredSchema now allows to instantiate arbitrarily many schematic symbols as well.

This implies a lots of syntax change on existing code, elthough it is mostly systematic. All proofs have been adapted to this new syntax.