changes to holSyntax to make it closer to the stateless version

put term_ok, type_ok, context_ok, and proves in mutual recursion.
remove axioms.