From 4ace54e64c3f18e80a3767590b3bd4a72f75be3a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 17 Nov 2022 18:05:33 +0100
Subject: [PATCH] Fix for
 https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/867#note_86458

---
 iris/program_logic/adequacy.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/iris/program_logic/adequacy.v b/iris/program_logic/adequacy.v
index ae781fa79..59c8e430d 100644
--- a/iris/program_logic/adequacy.v
+++ b/iris/program_logic/adequacy.v
@@ -230,7 +230,8 @@ Proof.
   rewrite replicate_length in Hlen2; subst.
   iDestruct (big_sepL2_length with "Hes'") as %Hlen3.
   rewrite -plus_n_O.
-  iApply ("Hφ" with "[//] [%] [ ] Hσ Hes'"); [congruence| |]; last first.
+  iApply ("Hφ" with "[//] [%] [ ] Hσ Hes'");
+    [by rewrite Hlen1 Hlen3| |]; last first.
   { by rewrite big_sepL2_replicate_r // big_sepL_omap. }
   (* we run the adequacy proof again to get this assumption *)
   iPureIntro. intros e2 -> Hel.
-- 
GitLab