delete some unnecessary proofs
tweak is_term_valuation_def and prove proves_consistent

i.e. if the theory context has a model, then it has both provable and
unprovable sequents. this is a simple corollary of soundness. the thing
remaining to show is that extensions of the initial context continue to
have models.