From 9fb4882f3effb2c6f2ed91fcb3077dde81a32cb0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 14 Jun 2016 15:04:18 +0200
Subject: [PATCH] Strenghen pair_op.

---
 algebra/cmra.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/algebra/cmra.v b/algebra/cmra.v
index abe9a0b2b..e01c27716 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -985,8 +985,7 @@ Section prod.
   Canonical Structure prodR :=
     CMRAT (A * B) prod_cofe_mixin prod_cmra_mixin.
 
-  Lemma pair_op (a a' : A) (b b' : B) :
-    (a, b) ⋅ (a', b') ≡ (a ⋅ a', b ⋅ b').
+  Lemma pair_op (a a' : A) (b b' : B) : (a, b) â‹… (a', b') = (a â‹… a', b â‹… b').
   Proof. done. Qed.
 
   Global Instance prod_cmra_total : CMRATotal A → CMRATotal B → CMRATotal prodR.
-- 
GitLab