diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 62a47dfb3b13dff9051fd407e7957fc228b2a8bd..f1e018e2d41bff8d70ea8f80c19a828b0acd8044 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Import auth gmap frac agree.
+From iris.algebra Require Import auth gmap frac agree csum excl.
 From iris.base_logic.lib Require Export own.
 From iris.bi.lib Require Import fractional.
 From iris.proofmode Require Import tactics.
@@ -7,21 +7,36 @@ Import uPred.
 
 Definition gen_heapUR (L V : Type) `{Countable L} : ucmraT :=
   gmapUR L (prodR fracR (agreeR (leibnizC V))).
+Definition gen_metaUR (L : Type) `{Countable L} : ucmraT :=
+  gmapUR L (agreeR gnameC).
+
 Definition to_gen_heap {L V} `{Countable L} : gmap L V → gen_heapUR L V :=
   fmap (λ v, (1%Qp, to_agree (v : leibnizC V))).
+Definition to_gen_meta `{Countable L} : gmap L gname → gen_metaUR L :=
+  fmap to_agree.
 
 (** The CMRA we need. *)
 Class gen_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapG {
   gen_heap_inG :> inG Σ (authR (gen_heapUR L V));
-  gen_heap_name : gname
+  gen_meta_inG :> inG Σ (authR (gen_metaUR L));
+  gen_meta_data_inG :> inG Σ (csumR (exclR unitC) (agreeR positiveC));
+  gen_heap_name : gname;
+  gen_meta_name : gname
 }.
 Arguments gen_heap_name {_ _ _ _ _} _ : assert.
+Arguments gen_meta_name {_ _ _ _ _} _ : assert.
 
-Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} :=
-  { gen_heap_preG_inG :> inG Σ (authR (gen_heapUR L V)) }.
+Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
+  gen_heap_preG_inG :> inG Σ (authR (gen_heapUR L V));
+  gen_meta_preG_inG :> inG Σ (authR (gen_metaUR L));
+  gen_meta_data_preG_inG :> inG Σ (csumR (exclR unitC) (agreeR positiveC));
+}.
 
-Definition gen_heapΣ (L V : Type) `{Countable L} : gFunctors :=
-  #[GFunctor (authR (gen_heapUR L V))].
+Definition gen_heapΣ (L V : Type) `{Countable L} : gFunctors := #[
+  GFunctor (authR (gen_heapUR L V));
+  GFunctor (authR (gen_metaUR L));
+  GFunctor (csumR (exclR unitC) (agreeR positiveC))
+].
 
 Instance subG_gen_heapPreG {Σ L V} `{Countable L} :
   subG (gen_heapΣ L V) Σ → gen_heapPreG L V Σ.
@@ -30,14 +45,30 @@ Proof. solve_inG. Qed.
 Section definitions.
   Context `{Countable L, hG : !gen_heapG L V Σ}.
 
-  Definition gen_heap_ctx (σ : gmap L V) : iProp Σ :=
-    own (gen_heap_name hG) (● (to_gen_heap σ)).
+  Definition gen_heap_ctx (σ : gmap L V) : iProp Σ := (∃ m,
+    ⌜ dom _ m ⊆ dom (gset L) σ ⌝ ∧
+    own (gen_heap_name hG) (● (to_gen_heap σ)) ∗
+    own (gen_meta_name hG) (● (to_gen_meta m)))%I.
 
   Definition mapsto_def (l : L) (q : Qp) (v: V) : iProp Σ :=
     own (gen_heap_name hG) (â—¯ {[ l := (q, to_agree (v : leibnizC V)) ]}).
   Definition mapsto_aux : seal (@mapsto_def). by eexists. Qed.
   Definition mapsto := mapsto_aux.(unseal).
   Definition mapsto_eq : @mapsto = @mapsto_def := mapsto_aux.(seal_eq).
+
+  Definition meta_token_def (l : L) : iProp Σ :=
+    (∃ γm, own (gen_meta_name hG) (◯ {[ l := to_agree γm ]}) ∗
+           own γm (Cinl (Excl ())))%I.
+  Definition meta_token_aux : seal (@meta_token_def). by eexists. Qed.
+  Definition meta_token := meta_token_aux.(unseal).
+  Definition meta_token_eq : @meta_token = @meta_token_def := meta_token_aux.(seal_eq).
+
+  Definition meta_def `{Countable A} (l : L) (x : A) : iProp Σ :=
+    (∃ γm, own (gen_meta_name hG) (◯ {[ l := to_agree γm ]}) ∗
+           own γm (Cinr (to_agree (encode x))))%I.
+  Definition meta_aux : seal (@meta_def). by eexists. Qed.
+  Definition meta {A dA cA} := meta_aux.(unseal) A dA cA.
+  Definition meta_eq : @meta = @meta_def := meta_aux.(seal_eq).
 End definitions.
 
 Local Notation "l ↦{ q } v" := (mapsto l q v)
@@ -51,6 +82,7 @@ Local Notation "l ↦ -" := (l ↦{1} -)%I (at level 20) : bi_scope.
 Section to_gen_heap.
   Context (L V : Type) `{Countable L}.
   Implicit Types σ : gmap L V.
+  Implicit Types m : gmap L gname.
 
   (** Conversion to heaps and back *)
   Lemma to_gen_heap_valid σ : ✓ to_gen_heap σ.
@@ -67,17 +99,25 @@ Section to_gen_heap.
   Lemma to_gen_heap_insert l v σ :
     to_gen_heap (<[l:=v]> σ) = <[l:=(1%Qp, to_agree (v:leibnizC V))]> (to_gen_heap σ).
   Proof. by rewrite /to_gen_heap fmap_insert. Qed.
-  Lemma to_gen_heap_delete l σ :
-    to_gen_heap (delete l σ) = delete l (to_gen_heap σ).
-  Proof. by rewrite /to_gen_heap fmap_delete. Qed.
+
+  Lemma to_gen_meta_valid m : ✓ to_gen_meta m.
+  Proof. intros l. rewrite lookup_fmap. by case (m !! l). Qed.
+  Lemma lookup_to_gen_meta_None m l : m !! l = None → to_gen_meta m !! l = None.
+  Proof. by rewrite /to_gen_meta lookup_fmap=> ->. Qed.
+  Lemma to_gen_meta_insert l m γm :
+    to_gen_meta (<[l:=γm]> m) = <[l:=to_agree γm]> (to_gen_meta m).
+  Proof. by rewrite /to_gen_meta fmap_insert. Qed.
 End to_gen_heap.
 
 Lemma gen_heap_init `{Countable L, !gen_heapPreG L V Σ} σ :
   (|==> ∃ _ : gen_heapG L V Σ, gen_heap_ctx σ)%I.
 Proof.
-  iMod (own_alloc (● to_gen_heap σ)) as (γ) "Hh".
+  iMod (own_alloc (● to_gen_heap σ)) as (γh) "Hh".
   { rewrite auth_auth_valid. exact: to_gen_heap_valid. }
-  iModIntro. by iExists (GenHeapG L V Σ _ _ _ γ).
+  iMod (own_alloc (● to_gen_meta ∅)) as (γm) "Hm".
+  { rewrite auth_auth_valid. exact: to_gen_meta_valid. }
+  iModIntro. iExists (GenHeapG L V Σ _ _ _ _ _ γh γm).
+  iExists ∅; simpl. iFrame "Hh Hm". by rewrite dom_empty_L.
 Qed.
 
 Section gen_heap.
@@ -85,6 +125,7 @@ Section gen_heap.
   Implicit Types P Q : iProp Σ.
   Implicit Types Φ : V → iProp Σ.
   Implicit Types σ : gmap L V.
+  Implicit Types m : gmap L gname.
   Implicit Types h g : gen_heapUR L V.
   Implicit Types l : L.
   Implicit Types v : V.
@@ -131,44 +172,74 @@ Section gen_heap.
     iApply (mapsto_valid l _ v2). by iFrame.
   Qed.
 
+  (** General properties of [meta] and [meta_token] *)
+  Global Instance meta_token_timeless l : Timeless (meta_token l).
+  Proof. rewrite meta_token_eq /meta_token_def. apply _. Qed.
+  Global Instance meta_timeless `{Countable A} l (x : A) : Timeless (meta l x).
+  Proof. rewrite meta_eq /meta_def. apply _. Qed.
+  Global Instance meta_persistent `{Countable A} l (x : A) : Persistent (meta l x).
+  Proof. rewrite meta_eq /meta_def. apply _. Qed.
+
+  Lemma meta_agree `{Countable A} l (x1 x2 : A) :
+    meta l x1 -∗ meta l x2 -∗ ⌜x1 = x2⌝.
+  Proof.
+    rewrite meta_eq /meta_def.
+    iDestruct 1 as (γm1) "[Hγm1 Hm1]"; iDestruct 1 as (γm2) "[Hγm2 Hm2]".
+    iAssert ⌜ γm1 = γm2 ⌝%I as %->.
+    { iDestruct (own_valid_2 with "Hγm1 Hγm2") as %Hγ; iPureIntro.
+      move: Hγ. rewrite -auth_frag_op op_singleton=> /auth_frag_valid /=.
+      rewrite singleton_valid. apply: agree_op_invL'. }
+    iDestruct (own_valid_2 with "Hm1 Hm2") as %Hγ; iPureIntro.
+    move: Hγ=> /agree_op_invL'. by intros ?%(inj _).
+  Qed.
+  Lemma meta_set `{Countable A} l (x : A) : meta_token l ==∗ meta l x.
+  Proof.
+    rewrite meta_token_eq meta_eq /meta_token_def /meta_def.
+    iDestruct 1 as (γm) "[Hγm Hm]". iExists γm. iFrame "Hγm".
+    iApply (own_update with "Hm"). by apply cmra_update_exclusive.
+  Qed.
+
+  (** Update lemmas *)
   Lemma gen_heap_alloc σ l v :
-    σ !! l = None → gen_heap_ctx σ ==∗ gen_heap_ctx (<[l:=v]>σ) ∗ l ↦ v.
+    σ !! l = None →
+    gen_heap_ctx σ ==∗ gen_heap_ctx (<[l:=v]>σ) ∗ l ↦ v ∗ meta_token l.
   Proof.
-    iIntros (?) "Hσ". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
+    iIntros (Hσl). rewrite /gen_heap_ctx mapsto_eq /mapsto_def meta_token_eq /meta_token_def /=.
+    iDestruct 1 as (m Hσm) "[Hσ Hm]".
     iMod (own_update with "Hσ") as "[Hσ Hl]".
     { eapply auth_update_alloc,
         (alloc_singleton_local_update _ _ (1%Qp, to_agree (v:leibnizC _)))=> //.
       by apply lookup_to_gen_heap_None. }
-    iModIntro. rewrite to_gen_heap_insert. iFrame.
+    iMod (own_alloc (Cinl (Excl ()))) as (γm) "Hγm"; first done.
+    iMod (own_update with "Hm") as "[Hm Hlm]".
+    { eapply auth_update_alloc.
+      eapply (alloc_singleton_local_update _ l (to_agree γm))=> //.
+      apply lookup_to_gen_meta_None.
+      move: Hσl. rewrite -!(not_elem_of_dom (D:=gset L)). set_solver. }
+    iModIntro. iFrame "Hl". iSplitL "Hσ Hm"; last by eauto with iFrame.
+    iExists (<[l:=γm]> m).
+    rewrite to_gen_heap_insert to_gen_meta_insert !dom_insert_L. iFrame.
+    iPureIntro. set_solver.
   Qed.
 
   Lemma gen_heap_alloc_gen σ σ' :
-    σ' ##ₘ σ → gen_heap_ctx σ ==∗ gen_heap_ctx (σ' ∪ σ) ∗ [∗ map] l ↦ v ∈ σ', l ↦ v.
-  Proof.
-    revert σ; induction σ' as [| l v σ' Hl IHσ'] using map_ind;
-      iIntros (σ Hσdisj) "Hσ".
-    - by rewrite left_id big_opM_empty; iFrame.
-    - iMod (IHσ' with "Hσ") as "[Hσ m]"; first by eapply map_disjoint_insert_l.
-      rewrite big_opM_insert //; iFrame.
-      assert (σ !! l = None).
-      { eapply map_disjoint_Some_r; first by eauto.
-        rewrite lookup_insert //. }
-      rewrite -insert_union_l //.
-      iMod (gen_heap_alloc with "Hσ") as "[$ $]"; last done.
-      apply lookup_union_None; split; auto.
-  Qed.
-
-  Lemma gen_heap_dealloc σ l v :
-    gen_heap_ctx σ -∗ l ↦ v ==∗ gen_heap_ctx (delete l σ).
+    σ' ##ₘ σ →
+    gen_heap_ctx σ ==∗
+    gen_heap_ctx (σ' ∪ σ) ∗ ([∗ map] l ↦ v ∈ σ', l ↦ v) ∗ ([∗ map] l ↦ _ ∈ σ', meta_token l).
   Proof.
-    iIntros "Hσ Hl". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
-    rewrite to_gen_heap_delete. iApply (own_update_2 with "Hσ Hl").
-    eapply auth_update_dealloc, (delete_singleton_local_update _ _ _).
+    revert σ; induction σ' as [| l v σ' Hl IH] using map_ind; iIntros (σ Hdisj) "Hσ".
+    { rewrite left_id_L. auto. }
+    iMod (IH with "Hσ") as "[Hσ'σ Hσ']"; first by eapply map_disjoint_insert_l.
+    decompose_map_disjoint.
+    rewrite !big_opM_insert // -insert_union_l //.
+    by iMod (gen_heap_alloc with "Hσ'σ") as "($ & $ & $)";
+      first by apply lookup_union_None.
   Qed.
 
   Lemma gen_heap_valid σ l q v : gen_heap_ctx σ -∗ l ↦{q} v -∗ ⌜σ !! l = Some v⌝.
   Proof.
-    iIntros "Hσ Hl". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
+    iDestruct 1 as (m Hσm) "[Hσ _]". iIntros "Hl".
+    rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
     iDestruct (own_valid_2 with "Hσ Hl")
       as %[Hl%gen_heap_singleton_included _]%auth_both_valid; auto.
   Qed.
@@ -176,13 +247,16 @@ Section gen_heap.
   Lemma gen_heap_update σ l v1 v2 :
     gen_heap_ctx σ -∗ l ↦ v1 ==∗ gen_heap_ctx (<[l:=v2]>σ) ∗ l ↦ v2.
   Proof.
-    iIntros "Hσ Hl". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
+    iDestruct 1 as (m Hσm) "[Hσ Hm]".
+    iIntros "Hl". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
     iDestruct (own_valid_2 with "Hσ Hl")
       as %[Hl%gen_heap_singleton_included _]%auth_both_valid.
     iMod (own_update_2 with "Hσ Hl") as "[Hσ Hl]".
     { eapply auth_update, singleton_local_update,
         (exclusive_local_update _ (1%Qp, to_agree (v2:leibnizC _)))=> //.
       by rewrite /to_gen_heap lookup_fmap Hl. }
-    iModIntro. rewrite to_gen_heap_insert. iFrame.
+    iModIntro. iFrame "Hl". iExists m. rewrite to_gen_heap_insert. iFrame.
+    iPureIntro. apply (elem_of_dom_2 (D:=gset L)) in Hl.
+    rewrite dom_insert_L. set_solver.
   Qed.
 End gen_heap.
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 991a35301c5774c31264d4748f3283d6c4b511fb..ca223901b2c90dad3288f8d2a479eca06928b5c7 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -32,7 +32,7 @@ Notation "l ↦{ q } -" := (∃ v, l ↦{q} v)%I
 Notation "l ↦ -" := (l ↦{1} -)%I (at level 20) : bi_scope.
 
 Definition array `{!heapG Σ} (l : loc) (vs : list val) : iProp Σ :=
-  ([∗ list] i ↦ v ∈ vs, loc_add l i ↦ v)%I.
+  ([∗ list] i ↦ v ∈ vs, (l +ₗ i) ↦ v)%I.
 Notation "l ↦∗ vs" := (array l vs)
   (at level 20, format "l  ↦∗  vs") : bi_scope.
 
@@ -218,7 +218,7 @@ Lemma array_singleton l v : l ↦∗ [v] ⊣⊢ l ↦ v.
 Proof. by rewrite /array /= right_id loc_add_0. Qed.
 
 Lemma array_app l vs ws :
-  l ↦∗ (vs ++ ws) ⊣⊢ l ↦∗ vs ∗ (loc_add l (length vs)) ↦∗ ws.
+  l ↦∗ (vs ++ ws) ⊣⊢ l ↦∗ vs ∗ (l +ₗ length vs) ↦∗ ws.
 Proof.
   rewrite /array big_sepL_app.
   setoid_rewrite Nat2Z.inj_add.
@@ -234,70 +234,82 @@ Proof.
 Qed.
 
 Lemma heap_array_to_array l vs :
-  ([∗ map] i ↦ v ∈ heap_array l vs, i ↦ v)%I -∗ l ↦∗ vs.
+  ([∗ map] l' ↦ v ∈ heap_array l vs, l' ↦ v) -∗ l ↦∗ vs.
 Proof.
-  iIntros "Hvs".
-  iInduction vs as [|v vs] "IH" forall (l); simpl.
-  { by rewrite big_opM_empty /array big_opL_nil. }
+  iIntros "Hvs". iInduction vs as [|v vs] "IH" forall (l); simpl.
+  { by rewrite /array. }
   rewrite big_opM_union; last first.
   { apply map_disjoint_spec=> l' v1 v2 /lookup_singleton_Some [-> _].
     intros (j&?&Hjl&_)%heap_array_lookup.
-    rewrite loc_add_assoc -{1}[l']loc_add_0 in Hjl;
-      apply loc_add_inj in Hjl; lia. }
+    rewrite loc_add_assoc -{1}[l']loc_add_0 in Hjl. simplify_eq; lia. }
   rewrite array_cons.
   rewrite big_opM_singleton; iDestruct "Hvs" as "[$ Hvs]".
   by iApply "IH".
 Qed.
 
+Lemma heap_array_to_seq_meta l vs n :
+  length vs = n →
+  ([∗ map] l' ↦ _ ∈ heap_array l vs, meta_token l') -∗
+  [∗ list] i ∈ seq 0 n, meta_token (l +ₗ (i : nat)).
+Proof.
+  iIntros (<-) "Hvs". iInduction vs as [|v vs] "IH" forall (l)=> //=.
+  rewrite big_opM_union; last first.
+  { apply map_disjoint_spec=> l' v1 v2 /lookup_singleton_Some [-> _].
+    intros (j&?&Hjl&_)%heap_array_lookup.
+    rewrite loc_add_assoc -{1}[l']loc_add_0 in Hjl. simplify_eq; lia. }
+  rewrite loc_add_0 -fmap_seq big_sepL_fmap.
+  setoid_rewrite Nat2Z.inj_succ. setoid_rewrite <-Z.add_1_l.
+  setoid_rewrite <-loc_add_assoc.
+  rewrite big_opM_singleton; iDestruct "Hvs" as "[$ Hvs]". by iApply "IH".
+Qed.
+
 (** Heap *)
 Lemma wp_allocN s E v n :
   0 < n →
   {{{ True }}} AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
-  {{{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v }}}.
+  {{{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v ∗
+         [∗ list] i ∈ seq 0 (Z.to_nat n), meta_token (l +ₗ (i : nat)) }}}.
 Proof.
   iIntros (Hn Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κ κs k) "[Hσ Hκs] !>"; iSplit; first by destruct n; auto with lia.
+  iIntros (σ1 κ κs k) "[Hσ Hκs] !>"; iSplit; first by auto with lia.
   iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
-  iMod (@gen_heap_alloc_gen with "Hσ") as "[Hσ Hl]".
+  iMod (@gen_heap_alloc_gen with "Hσ") as "(Hσ & Hl & Hm)".
   { apply (heap_array_map_disjoint _ l (replicate (Z.to_nat n) v)); eauto.
     rewrite replicate_length Z2Nat.id; auto with lia. }
-  iModIntro; iSplit; auto.
-  iFrame. iApply "HΦ".
-  by iApply heap_array_to_array.
+  iModIntro; iSplit; first done. iFrame "Hσ Hκs". iApply "HΦ". iSplitL "Hl".
+  - by iApply heap_array_to_array.
+  - iApply (heap_array_to_seq_meta with "Hm"). by rewrite replicate_length.
 Qed.
 Lemma twp_allocN s E v n :
   0 < n →
   [[{ True }]] AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
-  [[{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v }]].
+  [[{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v ∗
+         [∗ list] i ∈ seq 0 (Z.to_nat n), meta_token (l +ₗ (i : nat)) }]].
 Proof.
   iIntros (Hn Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κs k) "[Hσ Hκs] !>"; iSplit; first by destruct n; auto with lia.
   iIntros (κ v2 σ2 efs Hstep); inv_head_step.
-  iMod (@gen_heap_alloc_gen with "Hσ") as "[Hσ Hl]".
+  iMod (@gen_heap_alloc_gen with "Hσ") as "(Hσ & Hl & Hm)".
   { apply (heap_array_map_disjoint _ l (replicate (Z.to_nat n) v)); eauto.
     rewrite replicate_length Z2Nat.id; auto with lia. }
-  iModIntro; iSplit; auto.
-  iFrame; iSplit; auto. iApply "HΦ".
-  by iApply heap_array_to_array.
+  iModIntro; do 2 (iSplit; first done). iFrame "Hσ Hκs". iApply "HΦ". iSplitL "Hl".
+  - by iApply heap_array_to_array.
+  - iApply (heap_array_to_seq_meta with "Hm"). by rewrite replicate_length.
 Qed.
 
 Lemma wp_alloc s E v :
-  {{{ True }}} Alloc (Val v) @ s; E {{{ l, RET LitV (LitLoc l); l ↦ v }}}.
+  {{{ True }}} Alloc (Val v) @ s; E {{{ l, RET LitV (LitLoc l); l ↦ v ∗ meta_token l }}}.
 Proof.
-  iIntros (Φ) "_ HΦ".
-  iApply wp_allocN; auto with lia.
-  iNext; iIntros (l) "H".
-  iApply "HΦ".
-  by rewrite array_singleton.
+  iIntros (Φ) "_ HΦ". iApply wp_allocN; auto with lia.
+  iIntros "!>" (l) "/= (? & ? & _)".
+  rewrite array_singleton loc_add_0. iApply "HΦ"; iFrame.
 Qed.
 Lemma twp_alloc s E v :
-  [[{ True }]] Alloc (Val v) @ s; E [[{ l, RET LitV (LitLoc l); l ↦ v }]].
+  [[{ True }]] Alloc (Val v) @ s; E [[{ l, RET LitV (LitLoc l); l ↦ v ∗ meta_token l }]].
 Proof.
-  iIntros (Φ) "_ HΦ".
-  iApply twp_allocN; auto with lia.
-  iIntros (l) "H".
-  iApply "HΦ".
-  by rewrite array_singleton.
+  iIntros (Φ) "_ HΦ". iApply twp_allocN; auto with lia.
+  iIntros (l) "/= (? & ? & _)".
+  rewrite array_singleton loc_add_0. iApply "HΦ"; iFrame.
 Qed.
 
 Lemma wp_load s E l q v :
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 27db5d2c7f08ce51c7ed863c99e527e0b2f92406..fb2fe05141daf4ee990b5b2833584d0ad9405f1e 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -189,7 +189,7 @@ Proof.
   rewrite -wp_bind. eapply wand_apply; first exact: wp_allocN.
   rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l.
   destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
-  by rewrite right_id HΔ'.
+  apply wand_intro_l. by rewrite (sep_elim_l (l ↦∗ _)%I) right_id wand_elim_r.
 Qed.
 Lemma tac_twp_allocN Δ s E j K v n Φ :
   0 < n →
@@ -203,7 +203,7 @@ Proof.
   rewrite -twp_bind. eapply wand_apply; first exact: twp_allocN.
   rewrite left_id. apply forall_intro=> l.
   destruct (HΔ l) as (Δ'&?&HΔ'). rewrite envs_app_sound //; simpl.
-  by rewrite right_id HΔ'.
+  apply wand_intro_l. by rewrite (sep_elim_l (l ↦∗ _)%I) right_id wand_elim_r.
 Qed.
 
 Lemma tac_wp_alloc Δ Δ' s E j K v Φ :
@@ -217,7 +217,7 @@ Proof.
   rewrite -wp_bind. eapply wand_apply; first exact: wp_alloc.
   rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l.
   destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
-  by rewrite right_id HΔ'.
+  apply wand_intro_l. by rewrite (sep_elim_l (l ↦ v)%I) right_id wand_elim_r.
 Qed.
 Lemma tac_twp_alloc Δ s E j K v Φ :
   (∀ l, ∃ Δ',
@@ -229,7 +229,7 @@ Proof.
   rewrite -twp_bind. eapply wand_apply; first exact: twp_alloc.
   rewrite left_id. apply forall_intro=> l.
   destruct (HΔ l) as (Δ'&?&HΔ'). rewrite envs_app_sound //; simpl.
-  by rewrite right_id HΔ'.
+  apply wand_intro_l. by rewrite (sep_elim_l (l ↦ v)%I) right_id wand_elim_r.
 Qed.
 
 Lemma tac_wp_load Δ Δ' s E i K l q v Φ :