From 609c15c24e444f5a5cf788d393445ae39e3cd5ca Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 15 Sep 2020 21:39:26 +0200
Subject: [PATCH] Tweak proof.

---
 theories/base_logic/upred.v | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 845eb5ba5..874fed496 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -631,9 +631,7 @@ Proof. by unseal. Qed.
 
 Lemma prop_ext_2 P Q : ■ ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q.
 Proof.
-  unseal; split=> n x ? /= HPQ. split=> n' x' ??.
-    move: HPQ=> [] /(_ n' x'); rewrite !left_id=> ?.
-    move=> /(_ n' x'); rewrite !left_id=> ?. naive_solver.
+  unseal; split=> n x ? /=. setoid_rewrite (left_id ε op). split; naive_solver.
 Qed.
 
 (* The following two laws are very similar, and indeed they hold not just for â–¡
-- 
GitLab