From 36af3fe07f0922b8329e07afb88beaf764cbb4de Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 23 Jul 2023 10:13:46 +0200
Subject: [PATCH] Add lemma `cmra_opM_fmap_Some`.

---
 iris/algebra/cmra.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index 96b48dedc..88b3f79dd 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -1479,6 +1479,8 @@ Section option.
   Lemma cmra_opM_opM_swap_L `{!LeibnizEquiv A} a mb mc :
     a â‹…? mb â‹…? mc = a â‹…? mc â‹…? mb.
   Proof. by rewrite !cmra_opM_opM_assoc_L (comm_L _ mb). Qed.
+  Lemma cmra_opM_fmap_Some ma1 ma2 : ma1 â‹…? (Some <$> ma2) = ma1 â‹… ma2.
+  Proof. by destruct ma1, ma2. Qed.
 
   Global Instance Some_core_id a : CoreId a → CoreId (Some a).
   Proof. by constructor. Qed.
-- 
GitLab