define free_vars over :exp_exh
various lemmas about free_vars on :exp_pat

the main one, free_vars_pat_exp_to_pat, currently has many cheats