diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9314f0c344882c7c4a101ebe3bc98397131c4561..eb55cc22610e406d0ed6f3ccf90acb8de1652dac 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -153,6 +153,8 @@ API-breaking change is listed.
   `difference_insert`, `difference_insert_subseteq`. (by Hai Dang)
 - Tweak reduction on `gset`, so that `cbn` matches the behavior by `simpl` and
   does not unfold `gset` operations. (by Paolo G. Giarrusso, BedRock Systems)
+- 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`).
diff --git a/tests/tactics.v b/tests/tactics.v
index b91a47339b2dab2a042a985aae239ad53ed6629e..659f559b9ac07e9130943844a04fe65d25a35c63 100644
--- a/tests/tactics.v
+++ b/tests/tactics.v
@@ -82,3 +82,10 @@ Goal ∀ mx, mx = Some 10 → is_Some mx.
 Proof. done. Qed.
 Goal ∀ mx, Some 10 = mx → is_Some mx.
 Proof. done. Qed.
+
+(** get_head tests. *)
+Lemma test_get_head (f : nat → nat → nat → nat) : True.
+Proof.
+  let f' := get_head (f 0 1 2) in unify f f'.
+  let f' := get_head f in unify f f'.
+Abort.
diff --git a/theories/tactics.v b/theories/tactics.v
index 6ec949e0612abbc35a2c2ca994a7c028c850617f..78dbd9788085203f1174404ee0883e7442e05bdb 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -238,6 +238,14 @@ Ltac mk_evar T :=
   let _ := match goal with _ => clear e end in
   e'.
 
+(** The tactic [get_head t] returns the head function [f] when [t] is of the
+shape [f a1 ... aN]. This is purely syntactic, no unification is performed. *)
+Ltac get_head e :=
+  lazymatch e with
+  | ?h _ => get_head h
+  | _    => e
+  end.
+
 (** The tactic [eunify x y] succeeds if [x] and [y] can be unified, and fails
 otherwise. If it succeeds, it will instantiate necessary evars in [x] and [y].
 
@@ -412,17 +420,12 @@ Tactic Notation "f_equiv" "/=" := csimpl in *; f_equiv.
 we proceed by repeatedly using [f_equiv]. *)
 Ltac solve_proper_unfold :=
   (* Try unfolding the head symbol, which is the one we are proving a new property about *)
-  lazymatch goal with
-  | |- ?R (?f _ _ _ _ _ _ _ _ _ _) (?f _ _ _ _ _ _ _ _ _ _) => unfold f
-  | |- ?R (?f _ _ _ _ _ _ _ _ _) (?f _ _ _ _ _ _ _ _ _) => unfold f
-  | |- ?R (?f _ _ _ _ _ _ _ _) (?f _ _ _ _ _ _ _ _) => unfold f
-  | |- ?R (?f _ _ _ _ _ _ _) (?f _ _ _ _ _ _ _) => unfold f
-  | |- ?R (?f _ _ _ _ _ _) (?f _ _ _ _ _ _) => unfold f
-  | |- ?R (?f _ _ _ _ _) (?f _ _ _ _ _) => unfold f
-  | |- ?R (?f _ _ _ _) (?f _ _ _ _) => unfold f
-  | |- ?R (?f _ _ _) (?f _ _ _) => unfold f
-  | |- ?R (?f _ _) (?f _ _) => unfold f
-  | |- ?R (?f _) (?f _) => unfold f
+  try lazymatch goal with
+  | |- ?R ?t1 ?t2 =>
+    let h1 := get_head t1 in
+    let h2 := get_head t2 in
+    unify h1 h2;
+    unfold h1
   end.
 (** [solve_proper_prepare] does some preparation work before the main
 [solve_proper] loop.  Having this as a separate tactic is useful for debugging