prove context_ok implies term_ok for everything in the context

but this might not actually be what is required for proves_IMP's
remaining cases...