From 88e0b05b71f4dcc7eb25a29fe80ba08afc440415 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 13 Feb 2016 18:42:06 +0100
Subject: [PATCH] Internalize equality property for agree.

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

diff --git a/algebra/agree.v b/algebra/agree.v
index 626fdf7da..4c786de79 100644
--- a/algebra/agree.v
+++ b/algebra/agree.v
@@ -131,6 +131,8 @@ Lemma to_agree_car n (x : agree A) : ✓{n} x → to_agree (x n) ≡{n}≡ x.
 Proof. intros [??]; split; naive_solver eauto using agree_valid_le. Qed.
 
 (** Internalized properties *)
+Lemma agree_equivI {M} a b : (to_agree a ≡ to_agree b)%I ≡ (a ≡ b : uPred M)%I.
+Proof. split. by intros [? Hv]; apply (Hv n). apply: to_agree_ne. Qed.
 Lemma agree_validI {M} x y : ✓ (x ⋅ y) ⊑ (x ≡ y : uPred M).
 Proof. by intros r n _ ?; apply: agree_op_inv. Qed.
 End agree.
-- 
GitLab