diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index 2c3f212c77f3dc437c727ec15f0291f987f840a4..8d86ce50f63ea0b8689595c98bfcf8fe5980bd0e 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -167,9 +167,7 @@ Section code.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val' // tctx_hasty_val' //.
       iFrame. iSplitL "Hx".
       - iExists _. iFrame. by rewrite uninit_own vec_to_list_length.
-      - iExists (_ :: vl). rewrite heap_mapsto_vec_cons. iFrame.
-        (* FIXME: Why does calling `iFrame` twice even make a difference? *)
-        iFrame. eauto. }
+      - iExists (#false :: vl). rewrite heap_mapsto_vec_cons. iFrame; eauto. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.