fix error in type_to_deep

need to do tyvar_to_deep on type variables
work in progress on termsem_cert

thinking of making a function to prove term_ok (and type_ok) for the result of
term_to_deep, rather than trying to prove it on a case-by-case basis in a tactic