attempt to prove things about the shol semantics

first tried proving that the semantics of a term is a member of the
semantics of its type. this led to wanting to prove that the semantics
relation is functional (it won't be total, though). this led to various
tweaks to the semantics definition and also to the inference system -
requiring various terms to be welltyped and closed etc. still not
proved. the difficulty now is to show:

if INST tyin t and INST tyin' t have the same type, and the type
variables in t all appear in the type of t, then in fact INST tyin t =
INST tyin' t. intuitively, type instantiation only instantiates type
variables, and since the result types are equal and all the type
variables are in the original type, they must have been instantiated the
same way. but this means another proof about INST_CORE whose definition
is complicated because of checking for accidental variable capture...