From 2a89273d51958ed461360b6f8c4eec341ef36fdb Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 20 Jan 2021 12:42:14 +0100
Subject: [PATCH] add list_fmap_alt

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

diff --git a/theories/list.v b/theories/list.v
index 1ce46801..8977f94c 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -3461,6 +3461,10 @@ Section fmap.
     destruct (IH l) as (l1&l2&->&->&->); [done|]. by exists (x :: l1), l2.
   Qed.
 
+  Lemma list_fmap_alt l :
+    f <$> l = omap (λ x, Some (f x)) l.
+  Proof. induction l; simplify_eq/=; done. Qed.
+
   Lemma fmap_length l : length (f <$> l) = length l.
   Proof. by induction l; f_equal/=. Qed.
   Lemma fmap_reverse l : f <$> reverse l = reverse (f <$> l).
-- 
GitLab