From be74ad29c5d3921c6ac61a27af04825446c62d16 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 21 Nov 2016 09:26:58 +0100
Subject: [PATCH] Prove f <$> to_gmap x X = to_gmap (f x) X.

---
 prelude/gmap.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/prelude/gmap.v b/prelude/gmap.v
index cb73640f6..20faae2cb 100644
--- a/prelude/gmap.v
+++ b/prelude/gmap.v
@@ -159,6 +159,12 @@ Proof.
     elem_of_singleton; destruct (decide (i = j)); intuition.
 Qed.
 
+Lemma fmap_to_gmap `{Countable K} {A B} (f : A → B) (X : gset K) (x : A) :
+  f <$> to_gmap x X = to_gmap (f x) X.
+Proof.
+  apply map_eq; intros j. rewrite lookup_fmap, !lookup_to_gmap.
+  by simplify_option_eq.
+Qed.
 Lemma to_gmap_dom `{Countable K} {A B} (m : gmap K A) (y : B) :
   to_gmap y (dom _ m) = const y <$> m.
 Proof.
-- 
GitLab