rework holDerivationLib to use bare terms, not ===

the problem with === is that it hides the structure of the term
underneath, whereas the article will want access to it. terms of type
:type or :term in objects in the virtual machine's state should always
be fully ground applications of the constructors only.
minor bug fix for absTerm command
fix minor bug in remove command
fix betaConv

the inference system has a weaker version that only beta reduces the
same variable as in the abstraction, but the article format wants to
beta reduce a general term and do a substitution. the latter is a
derived rule.
fix bug in appThm
minor fixes for subst
allow alpha-equivalent axioms to be retrieved from the theory

the reader record has to do more work now, namely finding the
appropriate axiom and proving the alpha-equivalence
minor fix for assume
add :cpn to the datatypes that need EVAL support