Start toward removing the expression elaborator

The only thing that the expression elaboration did was to add module prefixes to
constructor names to make them globally unique. This shouldn't be necessary with
the cenv in closures. However the type soundness proof needs updating because
constructor names are no longer globally unique, however constructor/type name
pairs are.