prove {TYPE,TERM,THM}_CONS_EXTEND
hol_verification: prove new_basic_definition_thm

1 cheat left (for type definition)
prove new_basic_type_definition_thm
progress on bootstrap inst
start sketch of Arthan-style set theory
flesh out new set theory more
move lemma from sholSemantics into modelSet
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.
x86-64/x64Correct tweaked and renamed to bootstrap/bootstrap_lemmas
make semantics parametrised, prove semantics_11

unfortunately Hol_reln doesn't recognize that (mem,indset,ch) is a
parameter, so I now feed the arguments in one at a time. something about
this setup is making the simplifier extremely slow...
speed up proof of psholSemanticsTheory.semantics_11
bit more psholSemantics
more psholSemantics, up to sequent_def
finish psholSemanticsTheory
add INFINITY_AX to the stateless inference system

requires lots of definitions: connectives, quantifiers, ONE_ONE, and
ONTO.

cheat the soundness proofs.
some thoughts in the pshol world about how to prove it sound, but it's
looking tedious, and feels like it shouldn't be...
semantics of conjunction
semantics of implies, and work on forall
semantics of remaining boolean connectives

one_one and onto remain
prove INFINITY_AX_correct