Prove the side conditions for type printing

There is one cheat because the translator is not generating a good side
condition for num_to_dec_string (which comes from HOL, not from CakeML).