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.