Thread a module environment throigh the semantics.
Push a module environment throught the type system.

I used lots of cheats to get the proofs working, because I haven't yet
defined a good module type environment.
Started to work on module environment invariants.