From 30c12c95e6e99f67c6f0c2bd8b7b9f650acb93bf Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 4 Feb 2016 23:58:22 +0100
Subject: [PATCH] More indexed product properties.

---
 algebra/cmra.v | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/algebra/cmra.v b/algebra/cmra.v
index bc4b94d25..944d07d8e 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -602,7 +602,14 @@ Section iprod_cmra.
       eauto using iprod_insert_updateP with congruence.
   Qed.
 
-  Context `{∀ x, Empty (B x)}.
+  Context `{∀ x, Empty (B x)} `{∀ x, CMRAIdentity (B x)}.
+  Lemma iprod_op_singleton (x : A) (y1 y2 : B x) :
+    iprod_singleton x y1 ⋅ iprod_singleton x y2 ≡ iprod_singleton x (y1 ⋅ y2).
+  Proof.
+    intros x'; destruct (decide (x' = x)) as [->|].
+    * by rewrite iprod_lookup_op !iprod_lookup_singleton.
+    * by rewrite iprod_lookup_op !iprod_lookup_singleton_ne // left_id.
+  Qed.
   Lemma iprod_singleton_updateP x (P : B x → Prop) (Q : iprod B → Prop) y1 :
     y1 ~~>: P → (∀ y2, P y2 → Q (iprod_singleton x y2)) →
     iprod_singleton x y1 ~~>: Q.
-- 
GitLab