From b68ae8c4dfcd6f71de9e68b6366b0dc04fcab1a2 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 5 Jun 2023 09:32:42 +0000
Subject: [PATCH] Apply 2 suggestions.

---
 iris/base_logic/algebra.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/iris/base_logic/algebra.v b/iris/base_logic/algebra.v
index 6009ce806..9342291f9 100644
--- a/iris/base_logic/algebra.v
+++ b/iris/base_logic/algebra.v
@@ -121,16 +121,16 @@ Section upred.
     Lemma to_agree_uninjI x : ✓ x ⊢ ∃ a, to_agree a ≡ x.
     Proof. uPred.unseal. split=> n y _. exact: to_agree_uninjN. Qed.
 
-    (** If two [x y : agree O] compose to a [to_agree o], they are internally
-      equal, and also equal to the [to_agree o]. *)
+    (** Derived lemma: If two [x y : agree O] compose to a [to_agree o],
+      they are internally equal, and also equal to the [to_agree o]. *)
     Lemma agree_op_equiv_to_agreeI x y a :
       x ⋅ y ≡ to_agree a ⊢ x ≡ y ∧ y ≡ to_agree a.
     Proof.
       assert (x ⋅ y ≡ to_agree a ⊢ x ≡ y) as Hxy_equiv.
-      - etrans; last apply agree_validI.
+      { etrans; last apply agree_validI.
         rewrite internal_eq_sym.
         rewrite (internal_eq_rewrite _ _ (λ o, ✓ o)%I).
-        by rewrite -to_agree_validI bi.True_impl.
+        by rewrite -to_agree_validI bi.True_impl. }
       - apply bi.and_intro; first done.
         (** This is quite painful without [iRewrite] *)
         etrans; first (apply bi.and_intro; reflexivity).
-- 
GitLab