add get_head tactic and use it in solve_proper_unfold

Tactic taken from Simuliris, originally written by @msammler.

CHANGELOG.md

@@ -151,6 +151,8 @@ API-breaking change is listed.
   `map_filter_singleton_False`, `map_filter_comm`, `map_union_least`,
   `map_subseteq_difference_l`, `insert_difference`, `insert_difference'`,
   `difference_insert`, `difference_insert_subseteq`. (by Hai Dang)
+- Add `get_head` tactic to determine the syntactic head of a function
+  application term.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).