failing to prove things about definitions

the term_ok/type_ok/context_ok syntax doesn't admit adding something
onto the defs obviously enough - will have to think about a nice way to
proceed, but probably won't be a trivial change.

new_axiom is going to be omitted.