work on a bootstrap lemmas cheat

the one about equality types. this ought to be proved by better
automation in the translator, but maybe it's easier to just prove
manually for now...
main lemmas for LoadRev
removing typo
removing another typo
bit more progress on equality types theorem
refactor hol-light in preparation for direct stateful semantics

The code for the ITP'14 submission now mostly lives in
hol-light/stateless (and hol-light/set-theory). The plan is to make a
new version in hol-light/stateful.
more equality types theorem
inv strengthened, a few cheats proved
prove another equality types related cheat
LoadRev cheat-free
a few cheats removed
minor tweak
finish the equality types cheats

but some of the proofs are extremely slow
copy stateful hol syntax for experimentation

and slight refactor (pull the theorems out, leaving just the
definitions) plus add some comments

still thinking about how to handle contexts, signatures, axioms, etc.
type annotation missing
two more cheats removed
can_Print made stricter, compiler proofs updated
Remove some HOL-specific things from the Lem files

Not finished yet
Missed a file in the last commit
printing cheats removed