From 29e2f60682eff056bb7d6a53c135f46de9f4c906 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 30 Jun 2018 03:15:43 +0200
Subject: [PATCH] Lemma list_fmap_insert.

---
 theories/list.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/list.v b/theories/list.v
index 72dee9a4..87576f64 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2961,6 +2961,8 @@ Section fmap.
     intros Hi. rewrite list_lookup_fmap in Hi.
     destruct (l !! i) eqn:?; simplify_eq/=; eauto.
   Qed.
+  Lemma list_fmap_insert l i x: f <$> <[i:=x]>l = <[i:=f x]>(f <$> l).
+  Proof. revert i. by induction l; intros [|i]; f_equal/=. Qed.
   Lemma list_alter_fmap (g : A → A) (h : B → B) l i :
     Forall (λ x, f (g x) = h (f x)) l → f <$> alter g i l = alter h i (f <$> l).
   Proof. intros Hl. revert i. by induction Hl; intros [|i]; f_equal/=. Qed.
-- 
GitLab