Done with preservation sketch! Last case was exe.

The lemmas to investigate are:
- substitution lemma
- subtyping transitivity
- subtyping inversion