diff --git a/iris/program_logic/adequacy.v b/iris/program_logic/adequacy.v
index ae781fa791f05fce6e64f6b6ead3dd7191d73dbe..59c8e430d49e97b8dd021ea7103a75dacc8b1d37 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.