From ecff0735c1b34be5b706ce0d58fb566be3c23880 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 22 May 2016 21:59:41 +0200
Subject: [PATCH] =?UTF-8?q?Prove=20core=20=E2=88=85=20=E2=89=A1=20?=
 =?UTF-8?q?=E2=88=85.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

diff --git a/algebra/cmra.v b/algebra/cmra.v
index af75e124f..7a25c150f 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -344,6 +344,8 @@ Section unit.
   Proof. by intros x; rewrite (comm op) left_id. Qed.
   Global Instance cmra_unit_persistent : Persistent ∅.
   Proof. by rewrite /Persistent -{2}(cmra_core_l ∅) right_id. Qed.
+  Lemma cmra_core_unit : core (∅:A) ≡ ∅.
+  Proof. by rewrite -{2}(cmra_core_l ∅) right_id. Qed.
 End unit.
 
 (** ** Local updates *)
-- 
GitLab