From 6923de6656105319e154711d064883b66be890e4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 25 Nov 2016 17:45:07 +0100
Subject: [PATCH] Make auth_frag_op a Leibniz equality.

---
 algebra/auth.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/algebra/auth.v b/algebra/auth.v
index 482b1eb94..f6a5ae88d 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -193,7 +193,7 @@ Lemma auth_validI {M} (x : auth A) :
           end : uPred M).
 Proof. uPred.unseal. by destruct x as [[[]|]]. Qed.
 
-Lemma auth_frag_op a b : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b.
+Lemma auth_frag_op a b : â—¯ (a â‹… b) = â—¯ a â‹… â—¯ b.
 Proof. done. Qed.
 Lemma auth_frag_mono a b : a ≼ b → ◯ a ≼ ◯ b.
 Proof. intros [c ->]. rewrite auth_frag_op. apply cmra_included_l. Qed.
-- 
GitLab