tweak inference system

want term_ok t to imply welltyped t and type_ok (typeof t). so don't
need to list those latter conditions when already assuming term_ok.
prove ASSUME, REFL, and TRANS correct

after reorganising sholSemanticsScript.sml a little.
the semantics is unchanged, but the correctness theorems for the
inference rules are a little more principled now.

also, i've improved the definition of has_semantics: a term t has
semantics if any term valuation σ can be extended to another one σ' that
closes over the free variables of t, and t has semantics under σ'. this
was the real missing ingredient for TRANS, since the mid-point might
have had free variables that don't appear on either end. needed to prove
various theorems about SUBMAP as it applies to the semantics.