Working on HOL conservativity

Pushing on showing that removing constant definitions from a term
respects alpha equivalence. Relies on a stronger reflexivity theorem
(RACONV_REFL2) for alpha than the one in holSyntaxExtra. I'm not 100%
sure that it is true (I can't figure out how to remove the final cheat).