From 3a4a1be72faa7771743963b269ca86c88050ae7b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 20 Jan 2021 13:44:55 +0100
Subject: [PATCH] add map_fmap_omap

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index e9a70da5..96298f84 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -724,6 +724,13 @@ Proof.
   by destruct (m !! i) eqn:?; simpl; erewrite ?Hi by eauto.
 Qed.
 
+Lemma map_fmap_omap {A B C} (f : A → option B) (g : B → C) (m : M A) :
+  g <$> omap f m = omap (λ x, g <$> f x) m.
+Proof.
+  apply map_eq. intros i.
+  rewrite !lookup_fmap, !lookup_omap. destruct (m !! i); done.
+Qed.
+
 Lemma map_fmap_alt {A B} (f : A → B) (m : M A) :
   f <$> m = omap (λ x, Some (f x)) m.
 Proof.
-- 
GitLab