add get_head tactic and use it in solve_proper_unfold

Tactic taken from Simuliris, originally written by @msammler.