diff --git a/theories/tactics.v b/theories/tactics.v
index eb0b3969e41e71fa25961b09be691e24fa2bbbb5..eab260c2ee5f4ec0d9dd80c12680affe02401360 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -326,6 +326,8 @@ 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