From 4ea5f3e2117fec048c8d205870106483818b3141 Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Mon, 5 Jun 2023 11:36:40 +0200
Subject: [PATCH] Improve proof with assert, remove -.

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

diff --git a/iris/base_logic/algebra.v b/iris/base_logic/algebra.v
index 9342291f9..d6fc1bbc3 100644
--- a/iris/base_logic/algebra.v
+++ b/iris/base_logic/algebra.v
@@ -131,15 +131,15 @@ Section upred.
         rewrite internal_eq_sym.
         rewrite (internal_eq_rewrite _ _ (λ o, ✓ o)%I).
         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).
-        rewrite {1}Hxy_equiv. apply bi.impl_elim_r'.
-        erewrite (internal_eq_rewrite (x ⋅ y) _ (λ z, y ≡ z)%I); last solve_proper.
-        apply bi.impl_mono; last done.
-        rewrite internal_eq_sym.
-        erewrite (internal_eq_rewrite y _ (λ z, y ≡ z ⋅ y)%I); last solve_proper.
-        by rewrite agree_idemp -(internal_eq_refl True) bi.True_impl.
+      apply bi.and_intro; first done.
+      (** This is quite painful without [iRewrite] *)
+      etrans; first (apply bi.and_intro; reflexivity).
+      rewrite {1}Hxy_equiv. apply bi.impl_elim_r'.
+      erewrite (internal_eq_rewrite (x ⋅ y) _ (λ z, y ≡ z)%I); last solve_proper.
+      apply bi.impl_mono; last done.
+      rewrite internal_eq_sym.
+      erewrite (internal_eq_rewrite y _ (λ z, y ≡ z ⋅ y)%I); last solve_proper.
+      by rewrite agree_idemp -(internal_eq_refl True) bi.True_impl.
     Qed.
   End agree.
 
-- 
GitLab