some syntactic niceties in polySet
start version of hol semantics based on polySet

it looks like the main difference is going to be having to put an
is_model M assumption on almost every theorem... this would be much
nicer with locales.