From 2227cd66adcaddc84ba1121f9e7dae4e53086d56 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 3 Oct 2016 19:16:10 +0200
Subject: [PATCH] Non step-indexed laws about exclusive and Some.

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

diff --git a/algebra/cmra.v b/algebra/cmra.v
index 93ee00523..474b1af41 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -1201,6 +1201,11 @@ Section option.
     ✓{n} (my ⋅ Some x) → my = None.
   Proof. rewrite comm. by apply exclusiveN_Some_l. Qed.
 
+  Lemma exclusive_Some_l x `{!Exclusive x} my : ✓ (Some x ⋅ my) → my = None.
+  Proof. destruct my. move=> /(exclusive_l x) []. done. Qed.
+  Lemma exclusive_Some_r x `{!Exclusive x} my : ✓ (my ⋅ Some x) → my = None.
+  Proof. rewrite comm. by apply exclusive_Some_l. Qed.
+
   Lemma Some_included x y : Some x ≼ Some y ↔ x ≡ y ∨ x ≼ y.
   Proof. rewrite option_included; naive_solver. Qed.
   Lemma Some_included' `{CMRATotal A} x y : Some x ≼ Some y ↔ x ≡ y ∨ x ≼ y.
-- 
GitLab