diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index ee7b3562c885db645f9d649bddfd060bf47a6dda..a7d8d9aae59ee4ede605b614662b4c7fb33fc4f5 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1607,7 +1607,7 @@ Proof.
   destruct (Hm k) as [y ->]; [by eauto|]. by f_equal/=.
 Qed.
 
-Lemma map_zip_with_diag {A C} (f : A → A → C) m :
+Lemma map_zip_with_diag {A C} (f : A → A → C) (m : M A) :
   map_zip_with f m m = (λ x, f x x) <$> m.
 Proof.
   unfold map_zip_with. rewrite merge_diag by naive_solver.