attempt to fix semantics

When recursively taking the semantics of the term defining a new
constant or type operator, we need to allow for the possibility that
this term contains free type variables. For constants, this allows them
to be polymorphic. For type operators, this allows them to be applied to
arguments that contain type variables.

So, have to use a non-empty type valuation in the recursive calls.

But this potentially makes the semantics of defined type operators much
more complicated... I ran into what looks like a major problem when
trying to prove that if a type has semantics under one valuation then it
also has semantics under any other valuation that covers at least the
same variables, because, in the case of a defined type operator, the
witness term's semantics under the other valuation is not obviously
non-empty...