strengthen semantics_typeset theorem

previously: if a term has semantics mt and its type has semantics mty, then mt <: mty.
now: if a term has a semantics mt, then its type has semantics mty and mt <: mty.

i.e. have added that the types of terms with semantics always have semantics.