Elaborate terms in modules

[robrix]

Elaborating terms on entry into the module will allow stronger guarantees (“Module is correct by construction”).

[robrix]

It’s probably better to describe this as an ElaboratedModule or AnnotatedModule of AnnotatedTerms.