From 414b7b1e6b42aaf026c2781869280e8147d2161e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 29 Nov 2017 09:19:43 +0100
Subject: [PATCH] Another form of associativity for `opM`.

---
 theories/algebra/cmra.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 1323605d1..91d626f83 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1333,6 +1333,9 @@ Section option.
   Lemma op_is_Some mx my : is_Some (mx ⋅ my) ↔ is_Some mx ∨ is_Some my.
   Proof. rewrite -!not_eq_None_Some op_None. destruct mx, my; naive_solver. Qed.
 
+  Lemma cmra_opM_assoc' x my mz : x ⋅? my ⋅? mz ≡ x ⋅? (my ⋅ mz).
+  Proof. destruct my, mz; by rewrite /= -?assoc. Qed.
+
   Global Instance Some_core_id (x : A) : CoreId x → CoreId (Some x).
   Proof. by constructor. Qed.
   Global Instance option_core_id (mx : option A) :
-- 
GitLab