More Declarations Should Be Allowed In Mutual Blocks

I want all declarations to be allowed in mutual blocks, unless there is a good (documented) reason not to allow them. Arbitrary restrictions do not make the language easier to understand. Specifically, the following declarations would be nice:

  • Postulates.
  • Modules.