Wrote down the rest of the stlc lemmas

... quickly before somebody fixes the inconsistency and breaks all my
one-line proofs :)