diff --git a/heap_lang/heap_lang.v b/heap_lang/heap_lang.v
index 93f206bd90346544136a3a09b2dc86ba01ae97f1..5482c8e012b9fa59644b4021ebbf07389fa2ab1b 100644
--- a/heap_lang/heap_lang.v
+++ b/heap_lang/heap_lang.v
@@ -313,3 +313,10 @@ Proof.
     exists (heap_lang.fill K' e2''); rewrite heap_lang.fill_app; split; auto.
     econstructor; eauto.
 Qed.
+
+Global Instance heap_lang_ctx_item Ki :
+  LanguageCtx heap_lang (heap_lang.fill_item Ki).
+Proof.
+  change (LanguageCtx heap_lang (heap_lang.fill [Ki])).
+  by apply _.
+Qed.
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index 71116edeca8be5a019f84c233d02939df0d758c4..e89728dacf42c632d1841d94f0d3c382e018d5f7 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -13,7 +13,11 @@ Implicit Types K : ectx.
 (** Bind. *)
 Lemma wp_bind {E e} K Q :
   wp E e (λ v, wp E (fill K (of_val v)) Q) ⊑ wp E (fill K e) Q.
-Proof. apply wp_bind. Qed.
+Proof. apply weakestpre.wp_bind. Qed.
+
+Lemma wp_bindi {E e} Ki Q :
+  wp E e (λ v, wp E (fill_item Ki (of_val v)) Q) ⊑ wp E (fill_item Ki e) Q.
+Proof. apply weakestpre.wp_bind. Qed.
 
 (** Base axioms for core primitives of the language: Stateful reductions. *)
 Lemma wp_alloc_pst E σ e v Q :
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index c79b53174bb87a9b59784553acf7a7d8126f38a1..d5297a534633b8bbace109529d4973e01d7746e8 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -34,9 +34,9 @@ Module LiftingTests.
     rewrite -later_intro. apply forall_intro=>l.
     apply wand_intro_l. rewrite right_id. apply const_elim_l; move=>_.
     rewrite -later_intro. asimpl.
-    rewrite -(wp_bind [SeqCtx (Load (Loc _))]).
-    rewrite -(wp_bind [StoreRCtx (LocV _)]).
-    rewrite -(wp_bind [PlusLCtx _]).
+    rewrite -(wp_bindi (SeqCtx (Load (Loc _)))).
+    rewrite -(wp_bindi (StoreRCtx (LocV _))).
+    rewrite -(wp_bindi (PlusLCtx _)).
     rewrite -wp_load_pst; first (apply sep_intro_True_r; first done); last first.
     { by rewrite lookup_insert. } (* RJ TODO: figure out why apply and eapply fail. *)
     rewrite -later_intro. apply wand_intro_l. rewrite right_id.
@@ -75,7 +75,7 @@ Module LiftingTests.
     (* Go on. *)
     rewrite -(wp_let _ _ (FindPred' (LitNat n1) (Var 0) (LitNat n2) (FindPred $ LitNat n2))).
     rewrite -wp_plus. asimpl.
-    rewrite -(wp_bind [CaseCtx _ _]).
+    rewrite -(wp_bindi (CaseCtx _ _)).
     rewrite -!later_intro /=.
     apply wp_lt; intros Hn12.
     * (* TODO RJ: It would be better if we could use wp_if_true here
@@ -97,7 +97,7 @@ Module LiftingTests.
     ▷Q (LitNatV $ pred n) ⊑ wp E (App Pred (LitNat n)) Q.
   Proof.
     rewrite -wp_lam //. asimpl.
-    rewrite -(wp_bind [CaseCtx _ _]).
+    rewrite -(wp_bindi (CaseCtx _ _)).
     apply later_mono, wp_le=> Hn.
     - rewrite -wp_case_inl //.
       rewrite -!later_intro -wp_value' //.