Complete and correct elaboration of terms

value_definition now reuses functions introduced by elaboration of instances
Add a check that constrained type variables must have just been introduced by
an universal quantifier

Prettify

Add a test case