Made the type Term generic in the type of the decoration in each term
node. This has many consequences, including the need to get rid of the
Verum and Falsum formulas, so that each formula has at least one term.
Also cleared a number of warnings.