diff --git a/adequacy.v b/adequacy.v
index 77e674833029dd2d4d58ae7c588e5fbb306db61b..1cd713a040d9b4e1475939d93a4e4d112d556033 100644
--- a/adequacy.v
+++ b/adequacy.v
@@ -10,7 +10,7 @@ Class heapPreG Σ := HeapPreG {
 }.
 
 Definition heapΣ : gFunctors :=
-  #[irisΣ lrust_lang;
+  #[irisΣ state;
     GFunctor (constRF (authR heapUR));
     GFunctor (constRF (authR heap_freeableUR))].
 Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
diff --git a/heap.v b/heap.v
index 60e2966527f3f5412426cda08913d496cabb076c..9ce30f2f45d4ab0577c87bd1c19d9492e1d82846 100644
--- a/heap.v
+++ b/heap.v
@@ -1,7 +1,6 @@
 From iris.algebra Require Import cmra_big_op gmap frac dec_agree.
 From iris.algebra Require Import csum excl auth.
-From iris.base_logic Require Import big_op.
-From iris.program_logic Require Export invariants wsat.
+From iris.base_logic Require Import big_op lib.invariants.
 From iris.proofmode Require Export tactics.
 From lrust Require Export lifting.
 Import uPred.
diff --git a/lifetime.v b/lifetime.v
index 5ac177e435d90c6b86b7bc3ecd99901ff330e0e0..5c6da7ada3870ac55b02a7adf15b5ac3eb82e82d 100644
--- a/lifetime.v
+++ b/lifetime.v
@@ -1,5 +1,5 @@
-From iris.program_logic Require Export fancy_updates.
-From iris.program_logic Require Import invariants namespaces thread_local.
+From iris.base_logic.lib Require Export fancy_updates invariants namespaces thread_local.
+From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import tactics.
 
 Definition lftN := nroot .@ "lft".
@@ -156,13 +156,17 @@ Section lft.
   Proof. by rewrite lft_own_op Qp_div_2. Qed.
 
   Global Instance into_and_lft_own κ q :
-    IntoAnd false ([κ]{q}) ([κ]{q/2}) ([κ]{q/2}).
+    IntoAnd false [κ]{q} [κ]{q/2} [κ]{q/2}.
   Proof. by rewrite /IntoAnd lft_own_split. Qed.
 
   Global Instance from_sep_lft_own κ q :
-    FromSep ([κ]{q}) ([κ]{q/2}) ([κ]{q/2}).
+    FromSep [κ]{q} [κ]{q/2} [κ]{q/2}.
   Proof. by rewrite /FromSep -lft_own_split. Qed.
 
+  Global Instance frame_lft_own κ q :
+    Frame [κ]{q/2} [κ]{q} [κ]{q/2} | 100.
+  Proof. by rewrite /Frame -lft_own_split. Qed.
+
   Lemma lft_borrow_open' E κ P q :
     nclose lftN ⊆ E →
       &{κ}P ⊢ [κ]{q} ={E}=★ ▷ P ★ (▷ P ={E}=★ &{κ}P ★ [κ]{q}).
diff --git a/lifting.v b/lifting.v
index 3c3159dcad04aa32a46b53e97773929b7fefb3ad..a6646a457608e7eb42619f21c7f633503d59b50b 100644
--- a/lifting.v
+++ b/lifting.v
@@ -1,5 +1,5 @@
 From iris.program_logic Require Export weakestpre.
-From iris.program_logic Require Import ectx_lifting wsat. (* for ownP *)
+From iris.program_logic Require Import ectx_lifting.
 From lrust Require Export lang.
 From lrust Require Import tactics.
 From iris.proofmode Require Import tactics.
diff --git a/memcpy.v b/memcpy.v
index d9046c30865b48c344dec197377758488c4ebc30..e67c09226653106ae6ed485f08b96218c514f782 100644
--- a/memcpy.v
+++ b/memcpy.v
@@ -1,3 +1,4 @@
+From iris.base_logic.lib Require Import namespaces.
 From lrust Require Export notation.
 From lrust Require Import heap proofmode.
 
diff --git a/perm.v b/perm.v
index 04f6898a549eebb59cafe9abe005616374ba0f95..6aeab7aee32a4c0df5da08c0cf597982203b1184 100644
--- a/perm.v
+++ b/perm.v
@@ -1,4 +1,3 @@
-From iris.program_logic Require Import thread_local.
 From iris.proofmode Require Import tactics.
 From lrust Require Export type proofmode.
 
diff --git a/perm_incl.v b/perm_incl.v
index 8ba71f507bf704f9b3d07c3c3633a25b36f9e2d6..20f49864de6db8b69db9ef8e03b551ce1cf18a5c 100644
--- a/perm_incl.v
+++ b/perm_incl.v
@@ -1,6 +1,5 @@
 From Coq Require Import Qcanon.
 From iris.base_logic Require Import big_op.
-From iris.program_logic Require Import thread_local.
 From lrust Require Export type perm.
 
 Import Perm Types.
@@ -107,12 +106,12 @@ Section props.
   Lemma perm_incl_share q ν κ ty :
     ν ◁ &uniq{κ} ty ★ [κ]{q} ⇒ ν ◁ &shr{κ} ty ★ [κ]{q}.
   Proof.
-    iIntros (tid) "[Huniq [Htok Hlft]]". unfold has_type.
+    iIntros (tid) "[Huniq [Htok $]]". unfold has_type.
     destruct (eval_expr ν); last by iDestruct "Huniq" as "[]".
     iDestruct "Huniq" as (l) "[% Hown]".
-    iMod (ty.(ty_share) _ lrustN with "Hown Htok") as "[Hown Htok]".
-    apply disjoint_union_l; solve_ndisj. set_solver. iModIntro.
-    iFrame. iExists _. iSplit. done. done.
+    iMod (ty.(ty_share) _ lrustN with "Hown Htok") as "[Hown $]".
+    apply disjoint_union_l; solve_ndisj. done. iModIntro.
+    simpl. eauto.
   Qed.
 
   Lemma split_own_prod tyl (q0: Qp) (ql : list Qp) (l : loc) tid :
@@ -228,10 +227,10 @@ Section props.
     destruct (eval_expr ν) as [[[|l|]|]|];
       try by (iDestruct "Hown" as "[]" || iDestruct "Hown" as (l) "[% _]").
     iDestruct "Hown" as (l') "[EQ [Hf Hown]]". iDestruct "EQ" as %[=]. subst l'.
-    iMod (lft_borrow_create with "Hκ Hown") as "[Hbor Hextract]". done.
+    iMod (lft_borrow_create with "Hκ Hown") as "[Hbor Hext]". done.
     iSplitL "Hbor". by simpl; eauto.
     iMod (lft_borrow_create with "Hκ Hf") as "[_ Hf]". done.
-    iMod (lft_extract_combine with "[-]"). done. by iFrame.
+    iMod (lft_extract_combine with "[$Hext $Hf]"). done.
     iModIntro. iApply lft_extract_mono; last done.
     iIntros "H/=". iExists _. iSplit. done. by iDestruct "H" as "[$$]".
   Qed.
diff --git a/proofmode.v b/proofmode.v
index 3518c7589dee59fb3a98ef37569a8268c258fc19..1b135df1160f1a12878e8757f61f00b01f276b5e 100644
--- a/proofmode.v
+++ b/proofmode.v
@@ -1,5 +1,6 @@
 From iris.proofmode Require Import coq_tactics.
 From iris.proofmode Require Export tactics.
+From iris.base_logic Require Import namespaces.
 From lrust Require Export wp_tactics heap.
 Import uPred.
 
diff --git a/type.v b/type.v
index cd6913e3d539d5f7376c99882d5f285756ddc904..3ef012f9ffd2e9aa1faa3f08bc41732ecc260e6e 100644
--- a/type.v
+++ b/type.v
@@ -1,5 +1,6 @@
 From iris.base_logic Require Import big_op.
-From iris.program_logic Require Import hoare thread_local.
+From iris.base_logic.lib Require Export thread_local.
+From iris.program_logic Require Import hoare.
 From lrust Require Export notation lifetime heap.
 
 Definition mgmtE := nclose tlN ∪ lftN.
@@ -35,8 +36,8 @@ Record type `{heapG Σ, lifetimeG Σ, thread_localG Σ} :=
       &{κ} (l ↦★: ty_own tid) ⊢ [κ]{q} ={E}=★ ty_shr κ tid N l ★ [κ]{q};
     ty_shr_mono κ κ' tid N l :
       κ' ⊑ κ ⊢ ty_shr κ tid N l → ty_shr κ' tid N l;
-    ty_shr_acc κ tid N E l q :
-      nclose N ⊆ E → mgmtE ⊆ E → ty_dup →
+    ty_shr_acc κ tid E N l q :
+      ty_dup → mgmtE ∪ nclose N ⊆ E →
       ty_shr κ tid N l ⊢
         [κ]{q} ★ tl_own tid N ={E}=★ ∃ q', ▷l ↦★{q'}: ty_own tid ★
            (▷l ↦★{q'}: ty_own tid ={E}=★ [κ]{q} ★ tl_own tid N)
@@ -76,7 +77,7 @@ Next Obligation.
   iExists vl. iFrame. by iApply (lft_frac_borrow_incl with "Hord").
 Qed.
 Next Obligation.
-  intros Σ??? st κ tid N E l q ???.  iIntros "#Hshr[Hlft $]".
+  intros Σ??? st κ tid N E l q ??.  iIntros "#Hshr[Hlft $]".
   iDestruct "Hshr" as (vl) "[Hf Hown]".
   iMod (lft_frac_borrow_open with "[] Hf Hlft") as (q') "[Hmt Hclose]";
     first set_solver.
@@ -152,7 +153,7 @@ Section types.
     iIntros (q ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
   Qed.
   Next Obligation.
-    intros q ty E N κ l tid q' ?? =>/=. iIntros "Hshr Htok".
+    move=> q ty E N κ l tid q' ?? /=. iIntros "Hshr Htok".
     iMod (lft_borrow_exists with "Hshr Htok") as (vl) "[Hb Htok]". set_solver.
     iMod (lft_borrow_split with "Hb") as "[Hb1 Hb2]". set_solver.
     iMod (lft_borrow_exists with "Hb2 Htok") as (l') "[Hb2 Htok]". set_solver.
@@ -204,7 +205,7 @@ Section types.
     iIntros (q ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
   Qed.
   Next Obligation.
-    intros κ ty E N κ' l tid q' ?? =>/=. iIntros "Hshr Htok".
+    move=> κ ty E N κ' l tid q' ??/=. iIntros "Hshr Htok".
     iMod (lft_borrow_exists with "Hshr Htok") as (vl) "[Hb Htok]". set_solver.
     iMod (lft_borrow_split with "Hb") as "[Hb1 Hb2]". set_solver.
     iMod (lft_borrow_exists with "Hb2 Htok") as (l') "[Hb2 Htok]". set_solver.
@@ -226,8 +227,7 @@ Section types.
         iApply lft_incl_trans. eauto. }
       iMod (lft_borrow_open with "Hb Htok") as "[Hown Hob]". set_solver.
       iIntros "!>". iNext.
-      iMod (lft_borrow_unnest with "Hκ''κ [Hown Hob]") as "[Htok Hb]". set_solver.
-        by iFrame.
+      iMod (lft_borrow_unnest with "Hκ''κ [$Hown $Hob]") as "[Htok Hb]". set_solver.
       iMod (ty.(ty_share) with "Hb Htok") as "[#Hshr Htok]"; try done.
       iMod ("Hclose" with "[]") as "_".
       (* FIXME : the "global sharing protocol" that we used for [own]
@@ -370,8 +370,7 @@ Section types.
     iSplit; last done. iIntros "!#*/=_#H'". by iApply (ty_shr_mono with "Hκ").
   Qed.
   Next Obligation.
-    intros tyl κ tid N E l q ?? DUP. setoid_rewrite split_prod_mt.
-    generalize 0%nat.
+    intros tyl κ tid E N l q DUP ?. setoid_rewrite split_prod_mt. generalize 0%nat.
     change (ndot (A:=nat)) with (λ N i, N .@ (0+i)%nat).
     destruct (split_prod_namespace tid N (length tyl)) as [Ef [EQ _]].
     setoid_rewrite ->EQ. clear EQ. generalize 0%nat.
@@ -381,22 +380,20 @@ Section types.
       iIntros (q i offs) "#Hshr([Htokh Htokq]&Htlf&Htlh&Htlq)".
       rewrite big_sepL_cons Nat.add_0_r.
       iDestruct "Hshr" as "[Hshrh Hshrq]". setoid_rewrite <-Nat.add_succ_comm.
-      iMod (IH with "Hshrq [Htokq Htlf Htlq]") as (q'q) "[Hownq Hcloseq]". by iFrame.
-      iMod (tyh.(ty_shr_acc) with "Hshrh [Htokh Htlh]") as (q'h) "[Hownh Hcloseh]"; try done.
-      by pose proof (nclose_subseteq N i); set_solver. by iFrame.
+      iMod (IH with "Hshrq [$Htokq $Htlf $Htlq]") as (q'q) "[Hownq Hcloseq]".
+      iMod (tyh.(ty_shr_acc) with "Hshrh [$Htokh $Htlh]") as (q'h) "[Hownh Hcloseh]".
+      by pose proof (nclose_subseteq N i); set_solver.
       destruct (Qp_lower_bound q'h q'q) as (q' & q'0h & q'0q & -> & ->).
       iExists q'. iModIntro. rewrite big_sepL_cons.
       rewrite -heap_mapsto_vec_prop_op; last apply ty_size_eq.
-      iDestruct "Hownh" as "[Hownh0 Hownh1]".
+      iDestruct "Hownh" as "[$ Hownh1]".
       rewrite (big_sepL_proper (λ _ x, _ ↦★{_}: _)%I); last first.
       { intros. rewrite -heap_mapsto_vec_prop_op; last apply ty_size_eq.
         instantiate (1:=λ _ y, _). simpl. reflexivity. }
-      rewrite big_sepL_sepL. iDestruct "Hownq" as "[Hownq0 Hownq1]".
-      iSplitL "Hownh0 Hownq0". iNext. by iFrame.
+      rewrite big_sepL_sepL. iDestruct "Hownq" as "[$ Hownq1]".
       iIntros "[Hh Hq]". rewrite (lft_own_split κ q).
-      iMod ("Hcloseh" with "[Hh Hownh1]") as "($&$)". iNext. by iFrame.
-      iMod ("Hcloseq" with "[Hq Hownq1]") as "($&$&$)". iNext. by iFrame.
-      done.
+      iMod ("Hcloseh" with "[$Hh $Hownh1]") as "($&$)".
+      iApply "Hcloseq". by iFrame.
   Qed.
 
   Lemma split_sum_mt l tid q tyl :
@@ -450,8 +447,8 @@ Section types.
     intros n tyl Hn E N κ l tid q ??. iIntros "Hown Htok". rewrite split_sum_mt.
     iMod (lft_borrow_exists with "Hown Htok") as (i) "[Hown Htok]". set_solver.
     iMod (lft_borrow_split with "Hown") as "[Hmt Hown]". set_solver.
-    iMod ((nth i tyl emp).(ty_share) with "Hown Htok") as "[#Hshr Htok]"; try done.
-    iFrame. iExists i. iFrame "#". by iApply lft_borrow_fracture.
+    iMod ((nth i tyl emp).(ty_share) with "Hown Htok") as "[#Hshr $]"; try done.
+    iExists i. iFrame "#". by iApply lft_borrow_fracture.
   Qed.
   Next Obligation.
     intros n tyl Hn κ κ' tid N l. iIntros "#Hord H".
@@ -460,13 +457,13 @@ Section types.
     by iApply ((nth i tyl emp).(ty_shr_mono) with "Hord").
   Qed.
   Next Obligation.
-    intros n tyl Hn κ tid N E l q ?? Hdup%Is_true_eq_true.
+    intros n tyl Hn κ tid E N l q Hdup%Is_true_eq_true ?.
     iIntros "#H[[Htok1 Htok2] Htl]".
     setoid_rewrite split_sum_mt. iDestruct "H" as (i) "[Hshr0 Hshr]".
     iMod (lft_frac_borrow_open with "[] Hshr0 Htok1") as (q'1) "[Hown Hclose]". set_solver.
     { iIntros "!#". iIntros (q1 q2). rewrite heap_mapsto_op_eq. iSplit; eauto. }
-    iMod ((nth i tyl emp).(ty_shr_acc) with "Hshr [Htok2 Htl]")
-      as (q'2) "[Hownq Hclose']"; try done; [|by iFrame|].
+    iMod ((nth i tyl emp).(ty_shr_acc) with "Hshr [Htok2 $Htl]")
+      as (q'2) "[Hownq Hclose']"; try done.
     { edestruct nth_in_or_default as [| ->]; last done.
       rewrite ->forallb_forall in Hdup. auto using Is_true_eq_left. }
     destruct (Qp_lower_bound q'1 q'2) as (q' & q'01 & q'02 & -> & ->).
@@ -483,7 +480,7 @@ Section types.
       iMod ("Hclose" with "Hown") as "$".
       iCombine "Hownq1" "Hownq2" as "Hownq".
       rewrite heap_mapsto_vec_prop_op; last (by intros; apply sum_size_eq, Hn).
-      iApply ("Hclose'" with "Hownq").
+      by iApply "Hclose'".
   Qed.
 
   Program Definition uninit (n : nat) : type :=
diff --git a/type_incl.v b/type_incl.v
index 90a19164209c8ac080ce36a2f31236ea88c63b87..ce370a7fcab146b3e58ab7fa4f76903b50f46bf0 100644
--- a/type_incl.v
+++ b/type_incl.v
@@ -1,5 +1,5 @@
 From iris.base_logic Require Import big_op.
-From iris.program_logic Require Import thread_local hoare.
+From iris.program_logic Require Import hoare.
 From lrust Require Export type perm_incl.
 
 Import Types.
diff --git a/typing.v b/typing.v
index 3a6eb3fa2dfda11a99826008491d463a594cdf97..bbffb696e0c1082bf9a669c1be8ec2e37c9c7b38 100644
--- a/typing.v
+++ b/typing.v
@@ -1,4 +1,4 @@
-From iris.program_logic Require Import thread_local hoare.
+From iris.program_logic Require Import hoare.
 From lrust Require Export type perm notation memcpy.
 From lrust Require Import perm_incl proofmode.
 
@@ -171,14 +171,13 @@ Section typing.
   Qed.
 
   Definition consumes (ty : type) (ρ1 ρ2 : expr → perm) : Prop :=
-    ∀ ν tid Φ,
+    ∀ ν tid Φ E, mgmtE ∪ lrustN ⊆ E →
       ρ1 ν tid ★ tl_own tid ⊤ ★
       (∀ (l:loc) vl q,
         (length vl = ty.(ty_size) ★ eval_expr ν = Some #l ★ l ↦★{q} vl ★
-         |={mgmtE ∪ lrustN}▷=> (ty.(ty_own) tid vl ★
-            (l ↦★{q} vl ={mgmtE ∪ lrustN}=★ ρ2 ν tid ★ tl_own tid ⊤)))
+         |={E}▷=> (ty.(ty_own) tid vl ★ (l ↦★{q} vl ={E}=★ ρ2 ν tid ★ tl_own tid ⊤)))
        -★ Φ #l)
-      ⊢ WP ν @ mgmtE ∪ lrustN {{ Φ }}.
+      ⊢ WP ν @ E {{ Φ }}.
   (* FIXME : why isn't the notation context on the two last parameters not
      taken into account? *)
   Arguments consumes _%T _%P _%P.
@@ -186,26 +185,26 @@ Section typing.
   Lemma consumes_copy_own ty q:
     ty.(ty_dup) → consumes ty (λ ν, ν ◁ own q ty)%P (λ ν, ν ◁ own q ty)%P.
   Proof.
-    iIntros (? ν tid Φ) "(H◁ & Htl & HΦ)". iApply (has_type_wp with "[- $H◁]").
+    iIntros (? ν tid Φ E ?) "(H◁ & Htl & HΦ)". iApply (has_type_wp with "[- $H◁]").
     iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" 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).
-    iModIntro. iApply "HΦ". iFrame "★#%". iIntros "!>!>!>H↦!>".
+    iApply "HΦ". iFrame "★#%". iIntros "!>!>!>H↦!>".
     rewrite /has_type Hνv. iExists _. iSplit. done. iFrame. iExists vl. eauto.
   Qed.
 
   Lemma consumes_move ty q:
     consumes ty (λ ν, ν ◁ own q ty)%P (λ ν, ν ◁ own q (uninit ty.(ty_size)))%P.
   Proof.
-    iIntros (ν tid Φ) "(H◁ & Htl & HΦ)". iApply (has_type_wp with "[- $H◁]").
+    iIntros (ν tid Φ E ?) "(H◁ & Htl & HΦ)". iApply (has_type_wp with "[- $H◁]").
     iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" 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).
-    iModIntro. iApply "HΦ". iFrame "★#%". iIntros "!>!>!>H↦!>".
+    iApply "HΦ". iFrame "★#%". iIntros "!>!>!>H↦!>".
     rewrite /has_type Hνv. iExists _. iSplit. done. iFrame. iExists vl. eauto.
   Qed.
 
@@ -214,7 +213,7 @@ Section typing.
     consumes ty (λ ν, ν ◁ &uniq{κ}ty ★ κ' ⊑ κ ★ [κ']{q})%P
                 (λ ν, ν ◁ &uniq{κ}ty ★ κ' ⊑ κ ★ [κ']{q})%P.
   Proof.
-    iIntros (? ν tid Φ) "((H◁ & #H⊑ & Htok & #Hκ') & Htl & HΦ)".
+    iIntros (? ν tid Φ E ?) "((H◁ & #H⊑ & Htok & #Hκ') & Htl & HΦ)".
     iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l') "[Heq H↦]". iDestruct "Heq" as %[=->].
     iMod (lft_incl_trade with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
@@ -222,7 +221,7 @@ Section typing.
     iDestruct "H↦" as (vl) "[>H↦ #Hown]".
     iAssert (â–· (length vl = ty_size ty))%I with "[#]" as ">%".
       by rewrite ty.(ty_size_eq).
-    iModIntro. iApply "HΦ". iFrame "★#%". iIntros "!>!>!>H↦".
+    iApply "HΦ". iFrame "★#%". iIntros "!>!>!>H↦".
     iMod (lft_borrow_close with "[H↦] Hclose'") as "[H↦ Htok]". set_solver.
     { iExists _. by iFrame. }
     iMod ("Hclose" with "Htok") as "$". rewrite /has_type Hνv. iExists _. eauto.
@@ -233,7 +232,7 @@ Section typing.
     consumes ty (λ ν, ν ◁ &shr{κ}ty ★ κ' ⊑ κ ★ [κ']{q})%P
                 (λ ν, ν ◁ &shr{κ}ty ★ κ' ⊑ κ ★ [κ']{q})%P.
   Proof.
-    iIntros (? ν tid Φ) "((H◁ & #H⊑ & [Htok #Hκ']) & Htl & HΦ)".
+    iIntros (? ν tid Φ E ?) "((H◁ & #H⊑ & [Htok #Hκ']) & Htl & HΦ)".
     iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l') "[Heq #Hshr]". iDestruct "Heq" as %[=->].
     iMod (lft_incl_trade with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
@@ -245,8 +244,7 @@ Section typing.
     iAssert (â–· (length vl = ty_size ty))%I with "[#]" as ">%".
       by rewrite ty.(ty_size_eq).
     iModIntro. iApply "HΦ". iFrame "★#%". iIntros "!>!>!>H↦".
-    iMod ("Hclose'" with "[H↦]") as "[Htok $]".
-    { iExists _. by iFrame. }
+    iMod ("Hclose'" with "[H↦]") as "[Htok $]". iExists _; by iFrame.
     iMod ("Hclose" with "Htok") as "$". rewrite /has_type Hνv. iExists _. eauto.
   Qed.
 
@@ -254,14 +252,11 @@ Section typing.
     ty.(ty_size) = 1%nat → consumes ty ρ1 ρ2 →
     typed_step (ρ1 ν) (!ν) (λ v, v ◁ ty ★ ρ2 ν)%P.
   Proof.
-    iIntros (Hsz Hconsumes tid) "!#[#HEAP[??]]". wp_bind ν. iApply wp_mask_mono. done.
-    iApply Hconsumes. iFrame. iIntros (l vl q) "(%&%&H↦&Hupd)".
-    (* FIXME : I need to use [fupd_mask_mono], but I do not expect so. *)
-    iApply fupd_wp. iApply fupd_mask_mono. done. iMod "Hupd". iModIntro.
-    rewrite ->Hsz in *. destruct vl as [|v [|]]; try done.
+    iIntros (Hsz Hconsumes tid) "!#[#HEAP[??]]". wp_bind ν.
+    iApply Hconsumes. done. iFrame. iIntros (l vl q) "(%&%&H↦&Hupd)".
+    iMod "Hupd". rewrite ->Hsz in *. destruct vl as [|v [|]]; try done.
     rewrite heap_mapsto_vec_singleton. wp_read. rewrite /sep has_type_value.
-    (* FIXME : Idem. *)
-    iApply fupd_mask_mono. done. iMod "Hupd" as "[$ Hclose]". by iApply "Hclose".
+    iMod "Hupd" as "[$ Hclose]". by iApply "Hclose".
   Qed.
 
   Lemma typed_deref_uniq_borrow_own ty ν κ κ' q q':
@@ -269,20 +264,21 @@ Section typing.
                (!ν)
                (λ v, v ◁ &uniq{κ} ty ★ κ' ⊑ κ ★ [κ']{q})%P.
   Proof.
-    iIntros (tid) "!#(#HEAP & (H◁ & #H⊑ & Htok & #Hκ') & Htl)". wp_bind ν.
+    iIntros (tid) "!#(#HEAP & (H◁ & #H⊑ & Htok & #Hκ') & $)". wp_bind ν.
     iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]!>". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l) "[Heq H↦]". iDestruct "Heq" as %[=->].
     iMod (lft_incl_trade with "H⊑ Htok") as (q'') "[Htok Hclose]". done.
     iMod (lft_borrow_open with "H↦ Htok") as "[H↦ Hclose']". done.
     iDestruct "H↦" as (vl) "[>H↦ Hown]". iDestruct "Hown" as (l') "(>% & H† & Hown)".
     subst. rewrite heap_mapsto_vec_singleton. wp_read.
-    iMod (lft_borrow_close_stronger with "[H↦ H† Hown] Hclose' []") as "[Hbor Htok]". done.
-    { iCombine "H†" "Hown" as "H". iCombine "H↦" "H" as "H". iNext. iExact "H". }
-    { iIntros "!>(?&?&?)!>". iNext. rewrite -heap_mapsto_vec_singleton. iExists _.
-      iFrame. iExists _. by iFrame. }
-    iMod (lft_borrow_split with "Hbor") as "[_ Hbor]". done.
-    iMod (lft_borrow_split with "Hbor") as "[_ Hbor]". done.
-    iMod ("Hclose" with "Htok"). iFrame "#★". iIntros "!>". iExists _. eauto.
+    iMod (lft_borrow_close_stronger with "[H↦ H† Hown] Hclose' []") as "[Hbor Htok]";
+      first done; first 2 last.
+    - iMod (lft_borrow_split with "Hbor") as "[_ Hbor]". done.
+      iMod (lft_borrow_split with "Hbor") as "[_ Hbor]". done.
+      iMod ("Hclose" with "Htok") as "$". iFrame "#". iExists _. eauto.
+    - by iFrame "H↦ H†".
+    - iIntros "!>(?&?&?)!>". iNext. iExists _.
+      rewrite -heap_mapsto_vec_singleton. iFrame. iExists _. by iFrame.
   Qed.
 
   Lemma typed_deref_shr_borrow_own ty ν κ κ' q q':
@@ -290,14 +286,14 @@ Section typing.
                (!ν)
                (λ v, v ◁ &shr{κ} ty ★ κ' ⊑ κ ★ [κ']{q})%P.
   Proof.
-    iIntros (tid) "!#(#HEAP & (H◁ & #H⊑ & Htok & #Hκ') & Htl)". wp_bind ν.
+    iIntros (tid) "!#(#HEAP & (H◁ & #H⊑ & Htok & #Hκ') & $)". wp_bind ν.
     iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]!>". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l) "[Heq #H↦]". iDestruct "Heq" as %[=->].
     iMod (lft_incl_trade with "H⊑ Htok") as (q'') "[[Htok1 Htok2] Hclose]". done.
     iDestruct "H↦" as (vl) "[H↦b Hown]".
     iMod (lft_frac_borrow_open with "[] H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
     { iIntros "!#". iIntros (q1 q2). rewrite heap_mapsto_op_eq. iSplit; auto. }
-    iSpecialize ("Hown" $! _ with "Htok2"). iFrame "#★".
+    iSpecialize ("Hown" $! _ with "Htok2").
     iApply wp_strong_mono. reflexivity. iSplitL "Hclose Hclose'"; last first.
     - iApply (wp_frame_step_l _ heapN _ (λ v, l ↦{q'''} v ★ v = #vl)%I); try done.
       iSplitL "Hown"; last by wp_read; eauto.
@@ -314,9 +310,9 @@ Section typing.
       iMod "Hown". iModIntro. iMod "H". iModIntro. iNext.
       iMod "H". iApply fupd_mask_frame_r. set_solver. done.
     - iIntros (v) "([#Hshr Htok] & H↦ & %)". subst.
-      iMod ("Hclose'" with "[H↦]") as "Htok'". by eauto.
-      iCombine "Htok" "Htok'" as "Htok". iMod ("Hclose" with "Htok") as "$".
-      iExists _. eauto.
+      iMod ("Hclose'" with "[$H↦]") as "Htok'".
+      iMod ("Hclose" with "[$Htok $Htok']") as "$".
+      iFrame "#". iExists _. eauto.
   Qed.
 
   Lemma typed_deref_uniq_borrow_borrow ty ν κ κ' κ'' q:
@@ -324,7 +320,7 @@ Section typing.
                (!ν)
                (λ v, v ◁ &uniq{κ'} ty ★ κ ⊑ κ' ★ [κ]{q})%P.
   Proof.
-    iIntros (tid) "!#(#HEAP & (H◁ & #H⊑1 & [Htok #Hκ'] & #H⊑2) & Htl)". wp_bind ν.
+    iIntros (tid) "!#(#HEAP & (H◁ & #H⊑1 & [Htok #Hκ'] & #H⊑2) & $)". wp_bind ν.
     iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]!>". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l) "[Heq H↦]". iDestruct "Heq" as %[=->].
     iMod (lft_incl_trade with "H⊑1 Htok") as (q'') "[Htok Hclose]". done.
@@ -336,10 +332,10 @@ Section typing.
     iMod (lft_borrow_open with "H↦ Htok1") as "[>H↦ Hclose']". done.
     iMod (lft_borrow_open with "Hbor Htok2") as "[Hbor Hclose'']". done.
     rewrite heap_mapsto_vec_singleton. wp_read.
-    iMod (lft_borrow_close with "[H↦] Hclose'") as "[_ Htok1]". done. by auto.
-    iMod (lft_borrow_unnest with "H⊑2 [Hbor Hclose'']") as "[Htok2 Hbor]". done. by iFrame.
-    iCombine "Htok1" "Htok2" as "Htok". iMod ("Hclose" with "Htok") as "$". iFrame "★#".
-    iExists _. eauto.
+    iMod (lft_borrow_close with "[$H↦] Hclose'") as "[_ Htok1]". done.
+    iMod (lft_borrow_unnest with "H⊑2 [$Hbor $Hclose'']") as "[Htok2 Hbor]". done.
+    iMod ("Hclose" with "[$Htok1 $Htok2]") as "$".
+    iFrame "#". iExists _. eauto.
   Qed.
 
   Lemma typed_deref_shr_borrow_borrow ty ν κ κ' κ'' q:
@@ -347,16 +343,43 @@ Section typing.
                (!ν)
                (λ v, v ◁ &shr{κ'} ty ★ κ ⊑ κ' ★ [κ]{q})%P.
   Proof.
-    (* TODO : fix the definition of sharing unique borrows before. *)
-  Admitted.
+    iIntros (tid) "!#(#HEAP & (H◁ & #H⊑1 & [Htok #Hκ'] & #H⊑2) & $)". wp_bind ν.
+    iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]!>". iDestruct "Hνv" as %Hνv.
+    rewrite has_type_value. iDestruct "H◁" as (l) "[Heq Hshr]".
+    iDestruct "Heq" as %[=->]. iDestruct "Hshr" as (l') "[H↦ Hown]".
+    iMod (lft_incl_trade with "H⊑1 Htok") as (q') "[[Htok1 Htok2] Hclose]". done.
+    iMod (lft_frac_borrow_open with "[] H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
+    { iIntros "!#". iIntros (q1 q2). rewrite heap_mapsto_op_eq. iSplit; auto. }
+    iSpecialize ("Hown" $! _ _ with "[$H⊑2 $Htok2]"). iApply lft_incl_refl.
+    iApply wp_strong_mono. reflexivity. iSplitL "Hclose Hclose'"; last first.
+    - iApply (wp_frame_step_l _ heapN _ (λ v, l ↦{q''} v ★ v = #l')%I); try done.
+      iSplitL "Hown"; last by wp_read; eauto.
+      (* TODO : solving this goal is way too complicated compared
+         to what actually happens. *)
+      iAssert (|={mgmtE ∪ ⊤ ∖ (mgmtE ∪ lrustN), heapN}▷=> True)%I as "H".
+      { iApply fupd_mono. iIntros "H!>"; iExact "H".
+        iApply fupd_intro_mask; last done.
+        assert (Hdisj:nclose heapN ⊥ (mgmtE ∪ lrustN))
+          by (rewrite !disjoint_union_r; solve_ndisj).
+        set_solver. }
+      rewrite {3 4}(union_difference_L (mgmtE ∪ lrustN) ⊤); last done.
+      iApply fupd_trans. iApply fupd_mask_frame_r. set_solver.
+      iMod "Hown". iModIntro. iMod "H". iModIntro. iNext.
+      iMod "H" as "_". iApply fupd_mask_frame_r. set_solver. done.
+    - iIntros (v) "([#Hshr Htok] & H↦ & %)". subst.
+      iMod ("Hclose'" with "[$H↦]") as "Htok'".
+      iMod ("Hclose" with "[$Htok $Htok']") as "$".
+      iFrame "#". iExists _. eauto.
+  Qed.
 
   Definition update (ty : type) (ρ1 ρ2 : expr → perm) : Prop :=
-    ∀ ν tid Φ, ρ1 ν tid ★
+    ∀ ν tid Φ E, mgmtE ∪ lrustN ⊆ E →
+      ρ1 ν tid ★
       (∀ (l:loc) vl,
          (length vl = ty.(ty_size) ★ eval_expr ν = Some #l ★ l ↦★ vl ★
-         ∀ vl', l ↦★ vl' ★ ▷ (ty.(ty_own) tid vl') ={mgmtE ∪ lrustN}=★ ρ2 ν tid)
+         ∀ vl', l ↦★ vl' ★ ▷ (ty.(ty_own) tid vl') ={E}=★ ρ2 ν tid)
          -★ Φ #l)
-      ⊢ WP ν @ mgmtE ∪ lrustN {{ Φ }}.
+      ⊢ WP ν @ E {{ Φ }}.
   (* FIXME : why isn't the notation context on the two last parameters not
      taken into account? *)
   Arguments update _%T _%P _%P.
@@ -365,7 +388,7 @@ Section typing.
     ty1.(ty_size) = ty2.(ty_size) →
     update ty1 (λ ν, ν ◁ own q ty2)%P (λ ν, ν ◁ own q ty1)%P.
   Proof.
-    iIntros (Hsz ν tid Φ) "[H◁ HΦ]". iApply (has_type_wp with "[- $H◁]").
+    iIntros (Hsz ν tid Φ E ?) "[H◁ HΦ]". iApply (has_type_wp with "[- $H◁]").
     iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l) "(Heq & >H† & H↦)".
     iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
@@ -378,7 +401,7 @@ Section typing.
     update ty (λ ν, ν ◁ &uniq{κ} ty ★ κ' ⊑ κ ★ [κ']{q})%P
               (λ ν, ν ◁ &uniq{κ} ty ★ κ' ⊑ κ ★ [κ']{q})%P.
   Proof.
-    iIntros (ν tid Φ) "[(H◁ & #H⊑ & Htok & #Hκ) HΦ]".
+    iIntros (ν tid Φ E ?) "[(H◁ & #H⊑ & Htok & #Hκ) HΦ]".
     iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l) "(Heq & H↦)". iDestruct "Heq" as %[=->].
     iMod (lft_incl_trade with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
@@ -394,14 +417,12 @@ Section typing.
     ty.(ty_size) = 1%nat → update ty ρ1 ρ2 →
     typed_step (ρ1 ν1 ★ ν2 ◁ ty) (ν1 <- ν2) (λ _, ρ2 ν1).
   Proof.
-    (* FIXME : I need to use [fupd_mask_mono], but I do not expect so. *)
     iIntros (Hsz Hupd tid) "!#(#HEAP & [Hρ1 H◁] & $)". wp_bind ν1.
-    iApply wp_mask_mono. done. iApply Hupd. iFrame. iIntros (l vl) "(%&%&H↦&Hupd)".
+    iApply Hupd. done. iFrame. iIntros (l vl) "(%&%&H↦&Hupd)".
     rewrite ->Hsz in *. destruct vl as [|v[|]]; try done.
     wp_bind ν2. iApply (has_type_wp with "[- $H◁]"). iIntros (v') "[% H◁]!>".
     rewrite heap_mapsto_vec_singleton. wp_write.
-    iApply fupd_mask_mono. done. iApply ("Hupd" $! [_]).
-    rewrite heap_mapsto_vec_singleton has_type_value. iFrame.
+    rewrite -heap_mapsto_vec_singleton has_type_value. iApply "Hupd". by iFrame.
   Qed.
 
   Lemma typed_memcpy ρ1 ρ1' ρ2 ρ2' ty ν1 ν2:
@@ -409,15 +430,12 @@ Section typing.
     typed_step (ρ1' ν1 ★ ρ2' ν2) (ν1 <-{ty.(ty_size)} !ν2) (λ _, ρ1 ν1 ★ ρ2 ν2)%P.
   Proof.
     iIntros (Hupd Hcons tid) "!#(#HEAP&[H1 H2]&Htl)". wp_bind ν1.
-    iApply wp_mask_mono. done. iApply (Hupd with "[- $H1]").
+    iApply (Hupd with "[- $H1]"). done.
     iIntros (l vl) "(% & % & H↦ & Hupd)". wp_bind ν2.
-    iApply wp_mask_mono. done. iApply (Hcons with "[- $H2 $Htl]").
-    iIntros (l' vl' q) "(% & % & H↦' & Hcons)".
-    (* FIXME : I need to use [fupd_mask_mono], but I do not expect so. *)
-    iApply wp_fupd. iApply fupd_wp. iApply fupd_mask_mono. done. iMod "Hcons".
-    iApply wp_memcpy; last iFrame "★#"; try done. iNext. iIntros "[H↦ H↦']".
-    (* FIXME : Idem. *)
-    iApply fupd_mask_mono. done. iMod "Hcons" as "[Hown' Hcons]".
+    iApply (Hcons with "[- $H2 $Htl]"). done.
+    iIntros (l' vl' q) "(% & % & H↦' & Hcons)". iApply wp_fupd.
+    iMod "Hcons". iApply wp_memcpy; last iFrame "★#"; try done. iNext.
+    iIntros "[H↦ H↦']". iMod "Hcons" as "[Hown' Hcons]".
     iMod ("Hcons" with "H↦'") as "[$$]". iApply "Hupd". by iFrame.
   Qed.