diff --git a/heap.v b/heap.v
index cf583bec94eaf7aaf477f205726a4485f245d219..ae535269e0535e20c930488ff536296e47e9e3c0 100644
--- a/heap.v
+++ b/heap.v
@@ -373,10 +373,10 @@ Section heap.
   Lemma wp_free E (n:Z) l vl Φ :
     nclose heapN ⊆ E →
     n = length vl →
-    heap_ctx ★ l ↦★ vl ★ †l…(length vl) ★ ▷ (|={E}=> Φ (LitV LitUnit))
+    heap_ctx ★ ▷ l ↦★ vl ★ ▷ †l…(length vl) ★ ▷ (|={E}=> Φ (LitV LitUnit))
     ⊢ WP Free (Lit $ LitInt n) (Lit $ LitLoc l) @ E {{ Φ }}.
   Proof.
-    iIntros (??) "(#Hinv & Hmt & Hf & HΦ)". rewrite /heap_ctx /heap_inv.
+    iIntros (??) "(#Hinv & >Hmt & >Hf & HΦ)". rewrite /heap_ctx /heap_inv.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & REL)" "Hclose".
     iDestruct "REL" as %REL.
     rewrite heap_freeable_eq /heap_freeable_def.
diff --git a/proofmode.v b/proofmode.v
index 579dcd8f0ed92b73917abf447e87090ce1ef2e2c..bebdd65bae427b2d67f8741042ed878345ce674b 100644
--- a/proofmode.v
+++ b/proofmode.v
@@ -37,6 +37,23 @@ Proof.
   rewrite envs_app_sound //; simpl. by rewrite right_id HΔ'.
 Qed.
 
+Lemma tac_wp_free Δ Δ' Δ'' Δ''' E i1 i2 vl (n : Z) (n' : nat) l Φ :
+  (Δ ⊢ heap_ctx) → nclose heapN ⊆ E → n = length vl →
+  IntoLaterEnvs Δ Δ' →
+  envs_lookup i1 Δ' = Some (false, l ↦★ vl)%I →
+  envs_delete i1 false Δ' = Δ'' →
+  envs_lookup i2 Δ'' = Some (false, †l…n')%I →
+  envs_delete i2 false Δ'' = Δ''' →
+  n' = length vl →
+  (Δ''' ⊢ |={E}=> Φ (LitV LitUnit)) →
+  Δ ⊢ WP Free (Lit $ LitInt n) (Lit $ LitLoc l) @ E {{ Φ }}.
+Proof.
+  intros ?? -> ?? <- ? <- -> HΔ. rewrite -wp_free // -always_and_sep_l.
+  apply and_intro; first done.
+  rewrite into_later_env_sound -!later_sep; apply later_mono.
+  do 2 (rewrite envs_lookup_sound' //). by rewrite HΔ.
+Qed.
+
 Lemma tac_wp_read Δ Δ' E i l q v o Φ :
   (Δ ⊢ heap_ctx) → nclose heapN ⊆ E → o = Na1Ord ∨ o = ScOrd →
   IntoLaterEnvs Δ Δ' →
@@ -87,7 +104,7 @@ Tactic Notation "wp_alloc" ident(l) ident(vl) "as" constr(H) constr(Hf) :=
       [reshape_expr e ltac:(fun K e' =>
          match eval hnf in e' with Alloc _ => wp_bind_core K end)
       |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
-    eapply tac_wp_alloc with _ _ H Hf;
+    eapply tac_wp_alloc with _ H Hf;
       [iAssumption || fail "wp_alloc: cannot find heap_ctx"
       |solve_ndisj
       |try fast_done
@@ -102,6 +119,29 @@ Tactic Notation "wp_alloc" ident(l) ident(vl) "as" constr(H) constr(Hf) :=
 Tactic Notation "wp_alloc" ident(l) ident(vl) :=
   let H := iFresh in let Hf := iFresh in wp_alloc l vl as H Hf.
 
+Tactic Notation "wp_free" :=
+  lazymatch goal with
+  | |- _ ⊢ wp ?E ?e ?Q =>
+    first
+      [reshape_expr e ltac:(fun K e' =>
+         match eval hnf in e' with Free _ _ => wp_bind_core K end)
+      |fail 1 "wp_free: cannot find 'Free' in" e];
+    eapply tac_wp_free;
+      [iAssumption || fail "wp_free: cannot find heap_ctx"
+      |solve_ndisj
+      |try fast_done
+      |apply _
+      |let l := match goal with |- _ = Some (_, (?l ↦★ _)%I) => l end in
+       iAssumptionCore || fail "wp_read: cannot find" l "↦★ ?"
+      |env_cbv; reflexivity
+      |let l := match goal with |- _ = Some (_, († ?l … _)%I) => l end in
+       iAssumptionCore || fail "wp_read: cannot find †" l "… ?"
+      |env_cbv; reflexivity
+      |try fast_done
+      |wp_finish]
+  | _ => fail "wp_free: not a 'wp'"
+  end.
+
 Tactic Notation "wp_read" :=
   lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q =>
diff --git a/typing.v b/typing.v
index 86c9fcb3a1f97ee4eccb3e5523204f1b2aebb7ba..764f23155b5cfd6bf1c8de707d8e5bceebd90f2e 100644
--- a/typing.v
+++ b/typing.v
@@ -10,7 +10,8 @@ Section typing.
 
   (* TODO : good notations for [typed_step] and [typed_step_ty] ? *)
   Definition typed_step (ρ : perm) e (θ : Valuable.t → perm) :=
-    ∀ tid, {{ ρ tid ★ tl_own tid ⊤ }} e {{ v, θ (Some v) tid ★ tl_own tid ⊤ }}.
+    ∀ tid,
+      heap_ctx ⊢ {{ ρ tid ★ tl_own tid ⊤ }} e {{ v, θ (Some v) tid ★ tl_own tid ⊤ }}.
 
   (* FIXME : why isn't the notation context on the last parameter not
      taken into account? *)
@@ -20,27 +21,29 @@ Section typing.
     typed_step ρ e (λ ν, ν ◁ ty)%P.
 
   Definition typed_program (ρ : perm) e :=
-    ∀ tid, {{ ρ tid ★ tl_own tid ⊤ }} e {{ v, False }}.
+    ∀ tid, heap_ctx ⊢  {{ ρ tid ★ tl_own tid ⊤ }} e {{ v, False }}.
 
   Lemma typed_step_frame ρ e θ ξ:
     typed_step ρ e θ → typed_step (ρ ★ ξ) e (λ ν, θ ν ★ ξ)%P.
-  Proof. iIntros (Hwt tid) "!#[[?$]?]". iApply Hwt. by iFrame. Qed.
+  Proof.
+    iIntros (Hwt tid) "#HEAP!#[[?$]?]". iApply (Hwt with "HEAP"). by iFrame.
+  Qed.
 
   Lemma typed_step_exists {A} ρ θ e ξ:
     (∀ x:A, typed_step (ρ ★ θ x) e ξ) →
     typed_step (ρ ★ ∃ x, θ x) e ξ.
   Proof.
-    iIntros (Hwt tid) "!#[[Hρ Hθ]?]". iDestruct "Hθ" as (x) "Hθ".
-    iApply Hwt. by iFrame.
+    iIntros (Hwt tid) "#HEAP!#[[Hρ Hθ]?]". iDestruct "Hθ" as (x) "Hθ".
+    iApply (Hwt with "HEAP"). by iFrame.
   Qed.
 
   Lemma typed_step_bool ρ (b:Datatypes.bool) :
     typed_step_ty ρ #b bool.
-  Proof. iIntros (tid) "!#[_$]". wp_value. simpl. eauto. Qed.
+  Proof. iIntros (tid) "_!#[_$]". wp_value. simpl. eauto. Qed.
 
   Lemma typed_step_int ρ (z:Datatypes.nat) :
     typed_step_ty ρ #z int.
-  Proof. iIntros (tid) "!#[_$]". wp_value. simpl. eauto. Qed.
+  Proof. iIntros (tid) "_!#[_$]". wp_value. simpl. eauto. Qed.
 
   Lemma typed_step_fn {A n} `{Duplicable _ ρ, Closed (f :b: xl +b+ []) e} θ :
     length xl = n →
@@ -49,7 +52,7 @@ Section typing.
         typed_program (Some fv ◁ fn θ ★ (θ a vl) ★ ρ) (subst' f fv e')) →
     typed_step_ty ρ (Rec f xl e) (fn θ).
   Proof.
-    iIntros (Hn He tid) "!# [#Hρ $]". iApply (wp_value _ _ _ (RecV f xl e)).
+    iIntros (Hn He tid) "#HEAP !# [#Hρ $]". iApply (wp_value _ _ _ (RecV f xl e)).
     { simpl. destruct decide as [CL|?]. repeat f_equal. apply proof_irrel. done. }
     iLöb as "IH". iExists _. iSplit. done. iIntros (a vl) "!#[Hθ?]".
     assert (is_Some (subst_l xl (map of_val vl) e)) as [e' He'].
@@ -58,7 +61,7 @@ Section typing.
     iApply wp_rec; try done.
     { apply List.Forall_forall=>?. rewrite in_map_iff=>-[?[<- _]].
       rewrite to_of_val. eauto. }
-    iNext. iApply He. done. by iFrame "★#".
+    iNext. iApply (He with "HEAP"). done. by iFrame "★#".
   Qed.
 
   Lemma typed_step_cont {n} `{Closed (f :b: xl +b+ []) e} ρ θ :
@@ -68,7 +71,7 @@ Section typing.
         typed_program (Some fv ◁ cont (λ vl, ρ ★ θ vl)%P ★ (θ vl) ★ ρ) (subst' f fv e')) →
     typed_step_ty ρ (Rec f xl e) (cont θ).
   Proof.
-    iIntros (Hn He tid) "!# [Hρ $]". iApply (wp_value _ _ _ (RecV f xl e)).
+    iIntros (Hn He tid) "#HEAP !# [Hρ $]". iApply (wp_value _ _ _ (RecV f xl e)).
     { simpl. destruct decide as [CL|?]. repeat f_equal. apply proof_irrel. done. }
     iLöb as "IH". iExists _. iSplit. done. iIntros (vl) "Hθ ?".
     assert (is_Some (subst_l xl (map of_val vl) e)) as [e' He'].
@@ -77,7 +80,7 @@ Section typing.
     iApply wp_rec; try done.
     { apply List.Forall_forall=>?. rewrite in_map_iff=>-[?[<- _]].
       rewrite to_of_val. eauto. }
-    iNext. iApply He. done. iFrame. simpl.
+    iNext. iApply (He with "HEAP"). done. iFrame. simpl.
     iExists _. iSplit. done. iIntros (vl') "[Hρ Hθ] Htl".
     iDestruct ("IH" with "Hρ") as (f') "[Hf' IH']".
     iDestruct "Hf'" as %[=<-]. iApply ("IH'" with "Hθ Htl").
@@ -86,7 +89,7 @@ Section typing.
   Lemma typed_step_valuable e ty:
     typed_step_ty (Valuable.of_expr e ◁ ty) e ty.
   Proof.
-    iIntros (tid) "!#[H$]".
+    iIntros (tid) "_!#[H$]".
     destruct (Valuable.of_expr e) as [v|] eqn:Hv. 2:by iDestruct "H" as "[]".
     by iApply Valuable.of_expr_wp.
   Qed.
@@ -95,10 +98,10 @@ Section typing.
     typed_step_ty ρ1 e1 int → typed_step_ty ρ2 e2 int →
     typed_step_ty (ρ1 ★ ρ2) (BinOp PlusOp e1 e2) int.
   Proof.
-    iIntros (He1 He2 tid) "!#[[H1 H2]?]".
-    wp_bind e1. iApply wp_wand_r. iSplitR "H2". iApply He1; by iFrame.
+    iIntros (He1 He2 tid) "#HEAP!#[[H1 H2]?]".
+    wp_bind e1. iApply wp_wand_r. iSplitR "H2". iApply (He1 with "HEAP"); by iFrame.
     iIntros (v1) "[Hv1?]". iDestruct "Hv1" as (z1) "Hz1". iDestruct "Hz1" as %[=->].
-    wp_bind e2. iApply wp_wand_r. iSplitL. iApply He2; by iFrame.
+    wp_bind e2. iApply wp_wand_r. iSplitL. iApply (He2 with "HEAP"); by iFrame.
     iIntros (v2) "[Hv2?]". iDestruct "Hv2" as (z2) "Hz2". iDestruct "Hz2" as %[=->].
     wp_op. iFrame. by iExists _.
   Qed.
@@ -107,10 +110,10 @@ Section typing.
     typed_step_ty ρ1 e1 int → typed_step_ty ρ2 e2 int →
     typed_step_ty (ρ1 ★ ρ2) (BinOp MinusOp e1 e2) int.
   Proof.
-    iIntros (He1 He2 tid) "!#[[H1 H2]?]".
-    wp_bind e1. iApply wp_wand_r. iSplitR "H2". iApply He1; by iFrame.
+    iIntros (He1 He2 tid) "#HEAP!#[[H1 H2]?]".
+    wp_bind e1. iApply wp_wand_r. iSplitR "H2". iApply (He1 with "HEAP"); by iFrame.
     iIntros (v1) "[Hv1?]". iDestruct "Hv1" as (z1) "Hz1". iDestruct "Hz1" as %[=->].
-    wp_bind e2. iApply wp_wand_r. iSplitL. iApply He2; by iFrame.
+    wp_bind e2. iApply wp_wand_r. iSplitL. iApply (He2 with "HEAP"); by iFrame.
     iIntros (v2) "[Hv2?]". iDestruct "Hv2" as (z2) "Hz2". iDestruct "Hz2" as %[=->].
     wp_op. iFrame. by iExists _.
   Qed.
@@ -119,10 +122,10 @@ Section typing.
     typed_step_ty ρ1 e1 int → typed_step_ty ρ2 e2 int →
     typed_step_ty (ρ1 ★ ρ2) (BinOp LeOp e1 e2) bool.
   Proof.
-    iIntros (He1 He2 tid) "!#[[H1 H2]?]".
-    wp_bind e1. iApply wp_wand_r. iSplitR "H2". iApply He1; by iFrame.
+    iIntros (He1 He2 tid) "#HEAP!#[[H1 H2]?]".
+    wp_bind e1. iApply wp_wand_r. iSplitR "H2". iApply (He1 with "HEAP"); by iFrame.
     iIntros (v1) "[Hv1?]". iDestruct "Hv1" as (z1) "Hz1". iDestruct "Hz1" as %[=->].
-    wp_bind e2. iApply wp_wand_r. iSplitL. iApply He2; by iFrame.
+    wp_bind e2. iApply wp_wand_r. iSplitL. iApply (He2 with "HEAP"); by iFrame.
     iIntros (v2) "[Hv2?]". iDestruct "Hv2" as (z2) "Hz2". iDestruct "Hz2" as %[=->].
     iFrame. wp_op; intros _; by iExists _.
   Qed.
@@ -130,7 +133,7 @@ Section typing.
   Lemma typed_step_newlft ρ:
     typed_step ρ Newlft (λ _, ∃ α, [α]{1} ★ α ∋ top)%P.
   Proof.
-    iIntros (tid) "!#[_$]". wp_value. iVs lft_begin as (α) "[?#?]". done.
+    iIntros (tid) "_!#[_$]". wp_value. iVs lft_begin as (α) "[?#?]". done.
     iVs (lft_borrow_create with "[][]") as "[_?]". done. done.
     2:by iVsIntro; iExists α; iFrame. eauto.
   Qed.
@@ -138,7 +141,7 @@ Section typing.
   Lemma typed_step_endlft κ ρ:
     typed_step (κ ∋ ρ ★ [κ]{1}) Endlft (λ _, ρ)%P.
   Proof.
-    iIntros (tid) "!#[[Hextr [Htok #Hlft]]$]".
+    iIntros (tid) "_!#[[Hextr [Htok #Hlft]]$]".
     wp_bind (#() ;; #())%E.
     iApply (wp_wand_r _ _ (λ _, _ ★ True)%I). iSplitR "Hextr".
     iApply (wp_frame_step_l with "[-]"); try done.
@@ -147,4 +150,65 @@ Section typing.
     by wp_seq.
   Qed.
 
+  Lemma typed_step_alloc ρ (n : nat):
+    0 < n → typed_step_ty ρ (Alloc #n) (own 1 (uninit n)).
+  Proof.
+    iIntros (? tid) "#HEAP!#[_$]". wp_alloc l vl as "H↦" "H†". iIntros "!==>".
+    iExists _. iSplit. done. iNext. rewrite Nat2Z.id. iFrame.
+    apply (inj Z.of_nat) in H3. iExists _. iFrame. eauto.
+  Qed.
+
+  Lemma typed_step_free ty e:
+    typed_step (Valuable.of_expr e ◁ own 1 ty) (Free #ty.(ty_size) e) (λ _, top).
+  Proof.
+    iIntros (tid) "#HEAP!#[Hown$]".
+    destruct (Valuable.of_expr e) as [v|] eqn:EQv; last by iDestruct "Hown" as "[]".
+    wp_bind e. iApply Valuable.of_expr_wp. done.
+    iDestruct "Hown" as (l) "(Hv & >H† & H↦★:)". iDestruct "Hv" as %[=->].
+    iDestruct "H↦★:" as (vl) "[>H↦ Hown]".
+    rewrite ty_size_eq. iDestruct "Hown" as ">%". wp_free; eauto.
+  Qed.
+
+  Definition consumes (ty : type) (ρ1 ρ2 : Valuable.t → perm) : Prop :=
+    ∀ (l:loc) tid, ρ1 (Some #l) tid ★ tl_own tid ⊤ ={mgmtE ∪ lrustN}=>
+      ∃ vl q, length vl = ty.(ty_size) ★ l ↦★{q} vl ★
+        |={mgmtE ∪ lrustN}▷=> (ty.(ty_own) tid vl ★
+           (l ↦★{q} vl ={mgmtE ∪ lrustN}=★ ρ2 (Some #l) tid ★ tl_own tid ⊤)).
+  (* FIXME : why isn't the notation context on the two last parameters not
+     taken into account? *)
+  Arguments consumes _%T _%P _%P.
+
+  Lemma consumes_copy_own (ty : type) q :
+    ty.(ty_dup) → consumes ty (λ ν, ν ◁ own q ty)%P (λ ν, ν ◁ own q ty)%P.
+  Proof.
+    iIntros (? l tid) "[Hown Htl]". iDestruct "Hown" as (l') "[Heq [>H† H↦]]".
+    iDestruct "Heq" as %[=<-]. iDestruct "H↦" as (vl) "[>H↦ #Hown]".
+    iAssert (▷ (length vl = ty_size ty))%I with "[#]" as ">%".
+      by rewrite ty.(ty_size_eq).
+    iVsIntro. iExists _, _. iFrame "★#%". iIntros "!==>!>!==>H↦!==>".
+    iExists _. iSplit. done. iFrame. iExists vl. eauto.
+  Qed.
+
+  Lemma consumes_move (ty : type) q :
+    consumes ty (λ ν, ν ◁ own q ty)%P (λ ν, ν ◁ own q (uninit ty.(ty_size)))%P.
+  Proof.
+    iIntros (l tid) "[Hown Htl]". iDestruct "Hown" as (l') "[Heq [>H† H↦]]".
+    iDestruct "Heq" as %[=<-]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
+    iAssert (▷ (length vl = ty_size ty))%I with "[#]" as ">%".
+      by rewrite ty.(ty_size_eq).
+    iVsIntro. iExists _, _. iFrame "★#%". iIntros "!==>!>!==>H↦!==>".
+    iExists _. iSplit. done. iFrame. iExists vl. eauto.
+  Qed.
+
+  Lemma consumes_copy_uniq_borrow (ty : type) q :
+    ty.(ty_dup) → consumes ty (λ ν, ν ◁ own q ty)%P (λ ν, ν ◁ own q ty)%P.
+  Proof.
+    iIntros (? l tid) "[Hown Htl]". iDestruct "Hown" as (l') "[Heq [>H† H↦]]".
+    iDestruct "Heq" as %[=<-]. iDestruct "H↦" as (vl) "[>H↦ #Hown]".
+    iAssert (▷ (length vl = ty_size ty))%I with "[#]" as ">%".
+      by rewrite ty.(ty_size_eq).
+    iVsIntro. iExists _, _. iFrame "★#%". iIntros "!==>!>!==>H↦!==>".
+    iExists _. iSplit. done. iFrame. iExists vl. eauto.
+  Qed.
+
 End typing.
\ No newline at end of file