From 162755de0ab886f56faf95f497d20e4407b11ea9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 13 Jul 2019 11:51:54 +0200
Subject: [PATCH] shorten proof

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

diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index d948592e9..9858c033c 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1144,8 +1144,7 @@ Section prod.
     core (a, b) = (core a, core b).
   Proof.
     rewrite /core /core' {1}/pcore /=.
-    rewrite (cmra_pcore_core a). simpl.
-    rewrite (cmra_pcore_core b). done.
+    rewrite (cmra_pcore_core a) /= (cmra_pcore_core b). done.
   Qed.
 
   Global Instance prod_cmra_total : CmraTotal A → CmraTotal B → CmraTotal prodR.
-- 
GitLab