Remove some HOL conservativity cheats

Also add an assumption to term_image_term_union that the function
respects alpha equivalence, to rule out some simple counter-examples.