Started to put envC & envM in closures in the main semantics.

This is a bit of an experiment, but it should work like this:

- The main semantics has the module and closure environments in the
  closures.

- This should make like easy for the translator, and it shouldn't be too
  hard for the type soundness proof or the big/small step equivalence
  proof.

- The current semantics will be renamed to evaluate', and moved into the
  compiler correctness proof directory.

- The current evaluate' semantics will be dropped.

- The compiler proof will get an extra first step that says if a program
  does not raise an exception (in the new extended closure semantics),
  then it has the same result in evaluate'. The IL generation phase
  should be able to run from there without change (except for some
  renaming).

Thus, we get a nice semantics, don't have to alter the compiler proofs,
and get the removal of closure and module environments from the closures
as an optimisation phase (with the identity optimisation function, since
the source code isn't actually changes). In the future, we might be able
to remove other things from the closures here, too.