Finally got type soundness provedfor modules with signatures.

No cheats now.