From 1da4e7102ff758637bac2a92c67b1ce6fc0b5c9d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 16 Jan 2016 02:44:54 +0100
Subject: [PATCH] More about excl.

---
 modures/excl.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/modures/excl.v b/modures/excl.v
index c3367fccf..638290684 100644
--- a/modures/excl.v
+++ b/modures/excl.v
@@ -127,6 +127,10 @@ Proof.
 Qed.
 Canonical Structure exclRA : cmraT :=
   CMRAT excl_cofe_mixin excl_cmra_mixin excl_cmra_extend_mixin.
+Lemma excl_validN_inv_l n x y : ✓{S n} (Excl x ⋅ y) → y = ∅.
+Proof. by destruct y. Qed.
+Lemma excl_validN_inv_r n x y : ✓{S n} (x ⋅ Excl y) → x = ∅.
+Proof. by destruct x. Qed.
 
 (* Updates *)
 Lemma excl_update (x : A) y : ✓ y → Excl x ⇝ y.
-- 
GitLab