define sane version of TYPE_SUBST, progress on semantics_typeset

also prove typeset_closes_over: if a type has semantics, all its type
variables are in the domain of the valuation.
the new TYPE_SUBST (called tyinst) takes a finite map binding type
variable names to types, rather than a reversed association list of
pairs of types (requiring precondition that the domain is all
variables).