From ddd73df13410ec49fc9ff614837f09e8e4f9e0e7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 9 Mar 2020 10:27:16 +0100
Subject: [PATCH] Add lemma `fmap_map_seq`.

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index c3cc55cf..e1c7f17d 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2131,6 +2131,14 @@ Section map_seq.
     rewrite map_seq_app, map_seq_singleton.
     by rewrite insert_union_singleton_r by (by rewrite map_seq_snoc_disjoint).
   Qed.
+
+  Lemma fmap_map_seq {B} (f : A → B) start xs :
+    f <$> map_seq start xs = map_seq start (f <$> xs).
+  Proof.
+    revert start. induction xs as [|x xs IH]; intros start; csimpl.
+    { by rewrite fmap_empty. }
+    by rewrite fmap_insert, IH.
+  Qed.
 End map_seq.
 
 (** * Tactics *)
-- 
GitLab