improvements to term_to_cert

but thinking it would be better to have a general
recursive hypothesis-simplification function that can be applied at
well-chosen points