diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 51b05327302c1c7aa9dc21f82c157284e3ead109..f065292b944d6504e06c375dfc6094944500ef93 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -214,6 +214,13 @@ Section setoid.
   Proof.
     intros ? m m' ? k; rewrite !lookup_fmap. by apply option_fmap_proper.
   Qed.
+  Global Instance map_zip_with_proper `{Equiv B, Equiv C} (f : A → B → C) :
+    Proper ((≡) ==> (≡) ==> (≡)) f →
+    Proper ((≡) ==> (≡) ==> (≡)) (map_zip_with (M:=M) f).
+  Proof.
+    intros Hf m1 m1' Hm1 m2 m2' Hm2. apply merge_ext; try done.
+    destruct 1; destruct 1; repeat f_equiv; constructor || done.
+  Qed.
 End setoid.
 
 (** ** General properties *)