Adding more automation: extracting from a type context. Also, reformulated some of the proof rules, so that they can be applied without the consequence rule.

Note that the _L lemmas/class projections are always faster (and
prefered to be used) when possible.

Subtyping for fixpoints. This is probably not fully general, but I don't see anything else which is easy to state.

Also, changed the way we substitute lists, so that we do not need to to substitute de function name separately.
Parameters get substituted from right to left.

Fixpoint type. There are still a few TODO for the non-expansiveness of sums, products and functions.