prove all term_ok terms and stateless sequents are well-typed

hoping this is enough syntactic information to allow proves_IMP to be
proved without appeal to the soundness proof.