More progress on modules.

The semantics and type system is (mostly) there, but the proofs now all
need maintaining and extending.