Strengthen the semantics for ill-typed programs

structure S = struct
  datatype t = C
  val x = raise Div
  datatype t = D
end

now gives a type error, rather than the Div exception. This will
simplify the conLang verification and use.
Strengthen the semantics of Recclosure application

Raise a type error is the closure contains duplicate names in the
recursive function. This should help the patLang compilation.
Finished fixing up metatheory from semantic strengthenings
Merge branch 'cenv_close' of github.com:xrchz/vml into cenv_close
Toward making the ILs use the new type errors

The proofs don't all build at the moment