From 9008bf44ae95face1f4a1065d4f45b0842145af7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 16 Jan 2020 21:08:58 +0100
Subject: [PATCH] Add `map_zip_with_proper`.

---
 theories/fin_maps.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 51b05327..f065292b 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 *)
-- 
GitLab