Add a obvious corollary.
Add some partial proofs about properties of addition functions in T. Partial because agda started using all of the memory ever and I gave up.
Make the proof that denotational semantics commute with dynamic semantics go through.

Technically speaking, the proof that denotational semantics commute
with dynamic semantics already worked and, in fact, is totally
unchanged in this commit, which really is about proving that
*substitution* commutes with the denotational semantics.

Turns out that basically everything I had tried previously to prove
this was rubbish. Threw it all out and did something better.