diff --git a/iris/program_logic/adequacy.v b/iris/program_logic/adequacy.v
index 59c8e430d49e97b8dd021ea7103a75dacc8b1d37..72f78ee78b9a08733e93e00cb05ed222e2df231e 100644
--- a/iris/program_logic/adequacy.v
+++ b/iris/program_logic/adequacy.v
@@ -231,6 +231,8 @@ Proof.
   iDestruct (big_sepL2_length with "Hes'") as %Hlen3.
   rewrite -plus_n_O.
   iApply ("Hφ" with "[//] [%] [ ] Hσ Hes'");
+    (* FIXME: Different implicit types for [length] are inferred, so [lia] and
+    [congruence] do not work due to https://github.com/coq/coq/issues/16634 *)
     [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 *)