strengthen definition of def_ok slightly

make it say that the term associated with a type definition must be a
predicate
strengthen proves_IMP slightly

assert that all the deftms of a context_ok defs are term_ok in that
defs.
slow progress on TYPE_Tyapp

and copy lots of proofs from stateless to stateful - the constants
should really be shared.

it's possible TYPE_Tyapp should be solved by changing some definitions
rather than going through this tedious proof...