diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index 96b48dedc3eb5f5477e55e552c822603ca738e6a..88b3f79ddeb8d19eb7270d232b6573483e6f64dd 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.