Another stab at the semantics for stateless hol

This time doing it as a relation to avoid the termination proof, which
has the pleasant effect of also avoiding the cases of malformed syntax.

typeset (relating a type to a set) and semantics (relating a term to a
set) are both defined. the rules for defined constants and type
operators make use of INST
  - to reconcile the type of the constant with the type of its defining
    term (which may have more free type variables), and
  - to reconcile type variables in the witness for the type operator
    with the supplied type arguments.

Thus, the semantics treats its two environments (mapping term variables
to sets and type variables to sets) almost entirely schematically, only
explicitly updating the term variable map once (for the interpretation
of an abstraction's body), and explicitly using an empty term variable
environment for terms that should be closed (constant definitions and
type definition witness predicates). Mapping of type variables is done
by INST instead.