failing attempts to prove things about alpha convertible terms

Want to show two things:
  - For any closed term tm, there is a term tm' such that ACONV tm tm'
    and all the (bound) variables in tm' have distinct names.
  - For any closed term tm with distinctly named variables,
    INST tyin tm = simple_inst tyin tm.

Haven't been able to get very far on proving either of these.
Suggestions welcome.