Proved the semantics of a welltyped term is in its typeset

Also proved that all typesets are inhabited.

Required various further tweaks to the semantics.

For example, the semantics for (Comb t u) seems to require me to
explicitly state that the type of t has a model. And the semantics of
type definitions now does seem to require that I say the representing
type is non-empty.