define stateful inference system with full context

The context now may include any of the following kinds of things:
  type definition, constant specification,
  new type, new constant, or new axiom.

Define provability as a single relation (not in mutual recursion with
any others). Define terms/types in context, and well-formed contexts
(terms/types all ok in a linear sequence of context updates) separately.