unsuccessful attempt to define semantics for stateless hol

type definitions complicate things greatly.

for example, it looks like typeset and semantics have to be defined in
mutual recursion, since the set assigned to a new type depends on the
semantics of the term picking out the subset of the representing type.

and it's not at all obvious what to give for the abs and rep constants
that come with a type definition: probably modelSetTheory needs some
more theory about the existence of bijections and then we need to just
pick one.

also not sure about the right thing to do when trying to give semantics
to things that are malformed, since i haven't thought about how the
semantics is going to be used... presumably this will underlie the
definition of |=, which means the only check on it is the consistency
proof (together with testing what you can actually prove).