diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index 07c50ce4994bf2aa019f49c7b069e90d547b0443..e3122bfd9108fc9e7992f53fb98737a54de28483 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -39,10 +39,7 @@ Proof.
   destruct H0 as (l & -> & ? & -> & ?).
   rewrite -(of_to_val (Loc l) (LocV l)) // in H0.
   apply of_val_inj in H0 as ->.
-  simpl. iSplitL; last done.
-  (* FIXME: I should be able to do [iSpecialize "HΦ" l]. *)
-  (* FIXME: I should be able to do [iApply "HΦ" l]. *)
-  iApply "HΦ". iSplit; done.
+  simpl. iSplitL; last done. iApply "HΦ" {l}. iSplit; done.
 Qed.
 
 Lemma wp_load_pst E σ l v Φ :