Add some more invariants to the modLang wholeProg semantics