diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index ff7f0c7827bc61215a663e4d874d722f5634adb1..a9dad272987643ed1ffb41ec4bd1763108e43596 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -148,6 +148,7 @@ Section heap.
   Proof. by rewrite heap_mapsto_op_eq Qp_div_2. Qed.
 
   (** Weakest precondition *)
+  (* FIXME: try to reduce usage of wp_pvs. We're losing view shifts here. *)
   Lemma wp_alloc N E e v Φ :
     to_val e = Some v → nclose N ⊆ E →
     heap_ctx N ★ ▷ (∀ l, l ↦ v ={E}=★ Φ (LitV (LitLoc l))) ⊢ WP Alloc e @ E {{ Φ }}.
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index 934fd4731afe5d3075b614879c47ef1c66b400c0..ea1e9076f1321ecbc02b81de65cc1fda023af8d5 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -17,6 +17,11 @@ Lemma wp_bind {E e} K Φ :
   WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}.
 Proof. exact: wp_ectx_bind. Qed.
 
+Lemma wp_bindi {E e} Ki Φ :
+  WP e @ E {{ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }} ⊢
+     WP fill_item Ki e @ E {{ Φ }}.
+Proof. exact: weakestpre.wp_bind. Qed.
+
 (** Base axioms for core primitives of the language: Stateful reductions. *)
 Lemma wp_alloc_pst E σ e v Φ :
   to_val e = Some v →