From 0d981f4233c3d9da451eb9232930e2915e251bdf Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 15 Mar 2016 02:36:19 +0100
Subject: [PATCH] Add lemma dec_agree_core_id.

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

diff --git a/algebra/dec_agree.v b/algebra/dec_agree.v
index b21ef8044..b11932e59 100644
--- a/algebra/dec_agree.v
+++ b/algebra/dec_agree.v
@@ -45,6 +45,9 @@ Qed.
 Canonical Structure dec_agreeR : cmraT := discreteR dec_agree_ra.
 
 (* Some properties of this CMRA *)
+Lemma dec_agree_core_id (x : dec_agree A) : core x = x.
+Proof. done. Qed.
+
 Lemma dec_agree_ne a b : a ≠ b → DecAgree a ⋅ DecAgree b = DecAgreeBot.
 Proof. intros. by rewrite /= decide_False. Qed.
 
-- 
GitLab