Fix another FIXME.

The tactic `iFrame` frames the spatial context in order, it does not do repeat
`iFrame anyHyp`. As a result, when you have evars, things become ambigious

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.