diff --git a/adequacy.v b/adequacy.v
index 27f331573afc57d355f59766fb130126a44bff85..a7936698483a09a01c2bb92f48d31741a332aec8 100644
--- a/adequacy.v
+++ b/adequacy.v
@@ -21,10 +21,10 @@ Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
   adequate e σ φ.
 Proof.
   intros Hwp; eapply (wp_adequacy Σ). iIntros (?) "Hσ".
-  iVs (own_alloc (● to_heap σ)) as (vγ) "Hvγ".
+  iMod (own_alloc (● to_heap σ)) as (vγ) "Hvγ".
   { apply (auth_auth_valid (to_heap _)), to_heap_valid. }
-  iVs (own_alloc (● (∅ : heap_freeableUR))) as (fγ) "Hfγ"; first done.
+  iMod (own_alloc (● (∅ : heap_freeableUR))) as (fγ) "Hfγ"; first done.
   set (Hheap := HeapG _ _ _ _ vγ fγ).
-  iVs (inv_alloc heapN _ heap_inv with "[-]"); [iNext; iExists σ, ∅; by iFrame|].
+  iMod (inv_alloc heapN _ heap_inv with "[-]"); [iNext; iExists σ, ∅; by iFrame|].
   iApply (Hwp _). by rewrite /heap_ctx.
 Qed.
diff --git a/heap.v b/heap.v
index ae535269e0535e20c930488ff536296e47e9e3c0..44d19463261d36415bebf7ac7cb72ecc1e6ce37d 100644
--- a/heap.v
+++ b/heap.v
@@ -1,5 +1,6 @@
-From iris.algebra Require Import upred_big_op cmra_big_op gmap frac dec_agree.
+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.proofmode Require Export tactics.
 From lrust Require Export lifting.
@@ -306,7 +307,7 @@ Section heap.
   Lemma heap_alloc_vs σ l vl:
     (∀ m : Z, σ !! shift_loc l m = None) →
     own heap_name (● to_heap σ)
-    =r=> own heap_name (● to_heap (init_mem l vl σ))
+    ==★ own heap_name (● to_heap (init_mem l vl σ))
        ★ own heap_name (◯ [⋅ list] i ↦ v ∈ vl,
            {[shift_loc l i := (1%Qp, Cinr 0%nat, DecAgree v)]}).
   Proof.
@@ -332,17 +333,17 @@ Section heap.
   Proof.
     iIntros (??) "[#Hinv HΦ]". rewrite /heap_ctx /heap_inv.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
-    iApply wp_alloc_pst=> //.
-    iIntros "{$Hσ} !>"; iIntros (l σ') "(% & #Hσσ' & Hσ') !==>".
+    iApply wp_alloc_pst=> //. iNext.
+    iIntros "{$Hσ}"; iIntros (l σ') "(% & #Hσσ' & Hσ') !>".
     iDestruct "Hσσ'" as %(vl & HvlLen & Hvl).
     assert (vl ≠ []) by (intros ->; simpl in *; lia).
-    iVs (heap_alloc_vs with "[$Hvalσ]") as "[Hvalσ' Hmapsto]"; first done.
-    iVs (own_update _ (● hF) with "HhF") as "[HhF Hfreeable]".
+    iMod (heap_alloc_vs with "[$Hvalσ]") as "[Hvalσ' Hmapsto]"; first done.
+    iMod (own_update _ (● hF) with "HhF") as "[HhF Hfreeable]".
     { apply auth_update_alloc,
         (alloc_singleton_local_update _ (l.1) (1%Qp, inter (l.2) (Z.to_nat n))).
       - eauto using heap_freeable_rel_None.
       - split. done. apply inter_valid. }
-    iVs ("Hclose" with "[Hσ' Hvalσ' HhF]") as "_".
+    iMod ("Hclose" with "[Hσ' Hvalσ' HhF]") as "_".
     - iNext. iExists σ', _. subst σ'. iFrame. iPureIntro.
       rewrite HvlLen Nat2Z.id. auto using heap_freeable_rel_init_mem.
     - rewrite heap_freeable_eq /heap_freeable_def. iApply "HΦ".
@@ -352,7 +353,7 @@ Section heap.
   Lemma heap_free_vs l vl σ :
     own heap_name (● to_heap σ) ★ own heap_name (◯ [⋅ list] i ↦ v ∈ vl,
       {[shift_loc l i := (1%Qp, Cinr 0%nat, DecAgree v)]})
-    =r=> own heap_name (● to_heap (free_mem l (length vl) σ)).
+    ==★ own heap_name (● to_heap (free_mem l (length vl) σ)).
   Proof.
     rewrite -own_op. apply own_update, auth_update_dealloc.
     revert σ l. induction vl as [|v vl IH]=> σ l; [done|].
@@ -389,12 +390,12 @@ Section heap.
     assert (0 < n) by (subst n; by destruct vl).
     iApply (wp_free_pst _ σ); auto.
     { intros i. subst n. eauto using heap_freeable_is_Some. }
-    iIntros "{$Hσ} !> Hσ !==>".
-    iVs (heap_free_vs with "[Hmt Hvalσ]") as "Hvalσ".
+    iNext. iIntros "{$Hσ} Hσ !>".
+    iMod (heap_free_vs with "[Hmt Hvalσ]") as "Hvalσ".
     { rewrite heap_mapsto_vec_combine //. iFrame. }
-    iVs (own_update_2 with "[$HhF $Hf]") as "HhF".
+    iMod (own_update_2 with "[$HhF $Hf]") as "HhF".
     { apply auth_update_dealloc, (delete_singleton_local_update _ _ _). }
-    iVs ("Hclose" with "[-HΦ]") as "_"; last done.
+    iMod ("Hclose" with "[-HΦ]") as "_"; last done.
     iNext. iExists _, _. subst. rewrite Nat2Z.id. iFrame.
     eauto using heap_freeable_rel_free_mem.
   Qed.
@@ -439,16 +440,16 @@ Section heap.
     rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
     iDestruct (heap_mapsto_lookup with "[$Hvalσ $Hv]") as %[n Hσl].
-    iApply wp_read_sc_pst; first done. iIntros "{$Hσ} !> Hσ !==>".
-    iVs ("Hclose" with "[-Hv HΦ]"); last by iApply "HΦ".
+    iApply wp_read_sc_pst; first done. iNext. iIntros "{$Hσ} Hσ !>".
+    iMod ("Hclose" with "[-Hv HΦ]"); last by iApply "HΦ".
     iNext. iExists σ, hF. iFrame. eauto.
   Qed.
 
   Lemma heap_read_vs σ n1 n2 nf l q v:
     σ !! l = Some (RSt (n1 + nf), v) →
     own heap_name (● to_heap σ) ★ heap_mapsto_st (RSt n1) l q v
-    =r=> own heap_name (● to_heap (<[l:=(RSt (n2 + nf), v)]> σ))
-       ★ heap_mapsto_st (RSt n2) l q v.
+    ==★ own heap_name (● to_heap (<[l:=(RSt (n2 + nf), v)]> σ))
+        ★ heap_mapsto_st (RSt n2) l q v.
   Proof.
     intros Hσv. rewrite -!own_op to_heap_insert.
     eapply own_update, auth_update, singleton_local_update.
@@ -467,25 +468,25 @@ Section heap.
     iApply (wp_read_na1_pst E).
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
     iDestruct (heap_mapsto_lookup with "[$Hvalσ $Hv]") as %[n Hσl].
-    iVs (heap_read_vs _ 0 1 with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
-    iVs (pvs_intro_mask' (E∖heapN) ∅) as "Hclose'"; first set_solver.
-    iVsIntro. iExists σ, n, v. iFrame. iSplit; [done|]. iIntros "!> Hσ".
-    iVs "Hclose'" as "_". iVs ("Hclose" with "[Hσ Hvalσ HhF]") as "_".
+    iMod (heap_read_vs _ 0 1 with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
+    iMod (fupd_intro_mask' (E∖heapN) ∅) as "Hclose'"; first set_solver.
+    iModIntro. iExists σ, n, v. iFrame. iSplit; [done|]. iIntros "!> Hσ".
+    iMod "Hclose'" as "_". iMod ("Hclose" with "[Hσ Hvalσ HhF]") as "_".
     { iNext. iExists _, _. iFrame. eauto using heap_freeable_rel_stable. }
-    iVsIntro. clear dependent n σ hF.
+    iModIntro. clear dependent n σ hF.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
     iDestruct (heap_mapsto_lookup with "[$Hvalσ $Hv]") as %[n Hσl].
-    iApply wp_read_na2_pst; first done. iIntros "{$Hσ} !> Hσ !==>".
-    iVs (heap_read_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
-    iVs ("Hclose" with "[-Hv HΦ]") as "_"; last by iApply "HΦ".
+    iApply wp_read_na2_pst; first done. iNext. iIntros "{$Hσ} Hσ !>".
+    iMod (heap_read_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
+    iMod ("Hclose" with "[-Hv HΦ]") as "_"; last by iApply "HΦ".
     iNext. iExists _, hF. iFrame. eauto using heap_freeable_rel_stable.
   Qed.
 
   Lemma heap_write_vs σ st1 st2 l v v':
     σ !! l = Some (st1, v) →
     own heap_name (● to_heap σ) ★ heap_mapsto_st st1 l 1%Qp v
-    =r=> own heap_name (● to_heap (<[l:=(st2, v')]> σ))
-       ★ heap_mapsto_st st2 l 1%Qp v'.
+    ==★ own heap_name (● to_heap (<[l:=(st2, v')]> σ))
+        ★ heap_mapsto_st st2 l 1%Qp v'.
   Proof.
     intros Hσv. rewrite -!own_op to_heap_insert.
     eapply own_update, auth_update, singleton_local_update.
@@ -502,9 +503,9 @@ Section heap.
     rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
     iDestruct (heap_mapsto_lookup_1 with "[$Hvalσ $Hv]") as %?.
-    iApply wp_write_sc_pst; [done|]. iIntros "{$Hσ} !> Hσ !==>".
-    iVs (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
-    iVs ("Hclose" with "[-Hv HΦ]") as "_"; last by iApply "HΦ".
+    iApply wp_write_sc_pst; [done|]. iNext. iIntros "{$Hσ} Hσ !>".
+    iMod (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
+    iMod ("Hclose" with "[-Hv HΦ]") as "_"; last by iApply "HΦ".
     iNext. iExists _, hF. iFrame. eauto using heap_freeable_rel_stable.
   Qed.
 
@@ -518,17 +519,17 @@ Section heap.
     iApply (wp_write_na1_pst E).
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
     iDestruct (heap_mapsto_lookup_1 with "[$Hvalσ $Hv]") as %?.
-    iVs (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
-    iVs (pvs_intro_mask' (E∖heapN) ∅) as "Hclose'"; first set_solver.
-    iVsIntro. iExists σ, v'. iSplit; [done|]. iIntros "{$Hσ} !> Hσ".
-    iVs "Hclose'" as "_". iVs ("Hclose" with "[Hσ Hvalσ HhF]") as "_".
+    iMod (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
+    iMod (fupd_intro_mask' (E∖heapN) ∅) as "Hclose'"; first set_solver.
+    iModIntro. iExists σ, v'. iSplit; [done|]. iIntros "{$Hσ} !> Hσ".
+    iMod "Hclose'" as "_". iMod ("Hclose" with "[Hσ Hvalσ HhF]") as "_".
     { iNext. iExists _, _. iFrame. eauto using heap_freeable_rel_stable. }
-    iVsIntro. clear dependent σ hF.
+    iModIntro. clear dependent σ hF.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
     iDestruct (heap_mapsto_lookup_1 with "[$Hvalσ $Hv]") as %?.
-    iApply wp_write_na2_pst; [done|]. iIntros "{$Hσ} !> Hσ !==>".
-    iVs (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
-    iVs ("Hclose" with "[-Hv HΦ]"); last by iApply "HΦ".
+    iApply wp_write_na2_pst; [done|]. iNext. iIntros "{$Hσ} Hσ !>".
+    iMod (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
+    iMod ("Hclose" with "[-Hv HΦ]"); last by iApply "HΦ".
     iNext. iExists _, hF. iFrame. eauto using heap_freeable_rel_stable.
   Qed.
 
@@ -544,8 +545,8 @@ Section heap.
     iDestruct (heap_mapsto_lookup with "[$Hvalσ $Hv]") as %[n Hσl].
     iApply wp_cas_fail_pst; eauto.
     { by rewrite /= bool_decide_false. }
-    iIntros "{$Hσ} !> Hσ !==>".
-    iVs ("Hclose" with "[-Hv HΦ]") as "_"; last by iApply "HΦ".
+    iNext. iIntros "{$Hσ} Hσ !>".
+    iMod ("Hclose" with "[-Hv HΦ]") as "_"; last by iApply "HΦ".
     iNext. iExists _, hF. iFrame. eauto using heap_freeable_rel_stable.
   Qed.
 
@@ -564,8 +565,8 @@ Section heap.
     iDestruct (heap_mapsto_lookup with "[$Hvalσ $Hl1]") as %[n1 Hσl1].
     iApply wp_cas_fail_pst; eauto.
     { by rewrite /= bool_decide_false // Hσl1 Hσl'. }
-    iIntros "{$Hσ} !> Hσ !==>".
-    iVs ("Hclose" with "[-Hl Hl' Hl1 HΦ]") as "_"; last by iApply "HΦ"; iFrame.
+    iNext. iIntros "{$Hσ} Hσ !>".
+    iMod ("Hclose" with "[-Hl Hl' Hl1 HΦ]") as "_"; last by iApply "HΦ"; iFrame.
     iNext. iExists _, hF. by iFrame.
   Qed.
 
@@ -581,9 +582,9 @@ Section heap.
     iDestruct (heap_mapsto_lookup_1 with "[$Hvalσ $Hv]") as %?.
     iApply wp_cas_suc_pst; eauto.
     { by rewrite /= bool_decide_true. }
-    iIntros "{$Hσ} !> Hσ !==>".
-    iVs (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
-    iVs ("Hclose" with "[-Hv HΦ]"); last by iApply "HΦ"; iFrame.
+    iNext. iIntros "{$Hσ} Hσ !>".
+    iMod (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
+    iMod ("Hclose" with "[-Hv HΦ]"); last by iApply "HΦ"; iFrame.
     iNext. iExists _, hF. iFrame. eauto using  heap_freeable_rel_stable.
   Qed.
 
@@ -599,9 +600,9 @@ Section heap.
     iDestruct (heap_mapsto_lookup_1 with "[$Hvalσ $Hv]") as %?.
     iApply wp_cas_suc_pst; eauto.
     { by rewrite /= bool_decide_true. }
-    iIntros "{$Hσ} !> Hσ !==>".
-    iVs (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
-    iVs ("Hclose" with "[-Hv HΦ]"); last by iApply "HΦ"; iFrame.
+    iNext. iIntros "{$Hσ} Hσ !>".
+    iMod (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
+    iMod ("Hclose" with "[-Hv HΦ]"); last by iApply "HΦ"; iFrame.
     iNext. iExists _, hF. iFrame. eauto using  heap_freeable_rel_stable.
   Qed.
 End heap.
diff --git a/lifetime.v b/lifetime.v
index 04c4812c4b1778d10535a8e8a1f31c98a407bb84..e46aa786638beb1f957d67be73080704ff282d8c 100644
--- a/lifetime.v
+++ b/lifetime.v
@@ -1,5 +1,4 @@
-From iris.algebra Require Import upred_big_op.
-From iris.program_logic Require Export viewshifts pviewshifts.
+From iris.program_logic Require Export fancy_updates.
 From iris.program_logic Require Import invariants namespaces thread_local.
 From iris.proofmode Require Import tactics.
 
@@ -86,18 +85,18 @@ Section lft.
   Global Existing Instance lft_pers_borrow_own_timeless.
 
   (** Basic rules about lifetimes  *)
-  Axiom lft_begin : ∀ `(nclose lftN ⊆ E), True ={E}=> ∃ κ, [κ]{1} ★ lft κ.
+  Axiom lft_begin : ∀ `(nclose lftN ⊆ E), True ={E}=★ ∃ κ, [κ]{1} ★ lft κ.
   (* TODO : Do we really need a full mask here ? *)
   Axiom lft_end : ∀ κ, lft κ ⊢ [κ]{1} -★ |={⊤,∅}▷=> [†κ].
   Axiom lft_own_op : ∀ κ q1 q2, [κ]{q1} ★ [κ]{q2} ⊣⊢ [κ]{q1+q2}.
 
   (** Creating borrows and using them  *)
   Axiom lft_borrow_create :
-    ∀ `(nclose lftN ⊆ E) κ P, lft κ ⊢ ▷ P ={E}=> &{κ} P ★ κ ∋ P.
+    ∀ `(nclose lftN ⊆ E) κ P, lft κ ⊢ ▷ P ={E}=★ &{κ} P ★ κ ∋ P.
   Axiom lft_borrow_split :
-    ∀ `(nclose lftN ⊆ E) κ P Q, &{κ}(P ★ Q) ={E}=> &{κ}P ★ &{κ}Q.
+    ∀ `(nclose lftN ⊆ E) κ P Q, &{κ}(P ★ Q) ={E}=★ &{κ}P ★ &{κ}Q.
   Axiom lft_borrow_combine :
-    ∀ `(nclose lftN ⊆ E) κ P Q, &{κ}P ★ &{κ}Q ={E}=> &{κ}(P ★ Q).
+    ∀ `(nclose lftN ⊆ E) κ P Q, &{κ}P ★ &{κ}Q ={E}=★ &{κ}(P ★ Q).
   Axiom lft_borrow_open :
     ∀ `(nclose lftN ⊆ E) κ P q,
       &{κ}P ⊢ [κ]{q} ={E}=★ ▷ P ★ lft_open_borrow κ q P.
@@ -109,18 +108,18 @@ Section lft.
       lft_open_borrow κ q P ⊢ ▷ (▷Q ={⊤ ∖ nclose lftN}=★ ▷P)
       ={E}=★ lft_open_borrow κ q Q.
   Axiom lft_reborrow :
-    ∀ `(nclose lftN ⊆ E) κ κ' P, κ' ⊑ κ ⊢ &{κ}P ={E}=> &{κ'}P ★ κ' ∋ &{κ}P.
+    ∀ `(nclose lftN ⊆ E) κ κ' P, κ' ⊑ κ ⊢ &{κ}P ={E}=★ &{κ'}P ★ κ' ∋ &{κ}P.
   Axiom lft_borrow_unnest :
     ∀ `(nclose lftN ⊆ E) κ κ' P q',
-      κ' ⊑ κ ⊢ &{κ}P ★ lft_open_borrow κ' q' (&{κ}P) ={E}=> [κ']{q'} ★ &{κ'}P.
+      κ' ⊑ κ ⊢ &{κ}P ★ lft_open_borrow κ' q' (&{κ}P) ={E}=★ [κ']{q'} ★ &{κ'}P.
 
   (** Lifetime inclusion  *)
   Axiom lft_mkincl :
-    ∀ `(nclose lftN ⊆ E) κ κ' q, lft κ ⊢ &{κ'} [κ]{q} ={E}=> κ' ⊑ κ.
+    ∀ `(nclose lftN ⊆ E) κ κ' q, lft κ ⊢ &{κ'} [κ]{q} ={E}=★ κ' ⊑ κ.
   Axiom lft_incl_refl : ∀ κ, True ⊢ κ ⊑ κ.
   Axiom lft_incl_trans : ∀ κ κ' κ'', κ ⊑ κ' ∧ κ' ⊑ κ'' ⊢ κ ⊑ κ''.
   Axiom lft_incl_trade : ∀ `(nclose lftN ⊆ E) κ κ' q,
-      κ ⊑ κ' ⊢ [κ]{q} ={E}=> ∃ q', [κ']{q'} ★ ([κ']{q'} ={E}=★ [κ]{q}).
+      κ ⊑ κ' ⊢ [κ]{q} ={E}=★ ∃ q', [κ']{q'} ★ ([κ']{q'} ={E}=★ [κ]{q}).
   Axiom lft_borrow_incl : ∀ κ κ' P, κ' ⊑ κ ⊢ &{κ}P → &{κ'}P.
   Axiom lft_incl_lft_l : ∀ κ κ', κ ⊑ κ' ⊢ lft κ.
   Axiom lft_incl_lft_r : ∀ κ κ', κ ⊑ κ' ⊢ lft κ'.
@@ -128,13 +127,13 @@ Section lft.
   (** Extraction  *)
   (* Axiom lft_extract_split : ∀ κ P Q, κ ∋ (P ★ Q) ={E}=> κ ∋ P ★ κ ∋ Q .*)
   Axiom lft_extract_combine :
-    ∀ `(nclose lftN ⊆ E) κ P Q, κ ∋ P ★ κ ∋ Q ={E}=> κ ∋ (P ★ Q).
-  Axiom lft_extract_out : ∀ `(nclose lftN ⊆ E) κ P, [†κ] ⊢ κ ∋ P ={E}=> ▷ P.
+    ∀ `(nclose lftN ⊆ E) κ P Q, κ ∋ P ★ κ ∋ Q ={E}=★ κ ∋ (P ★ Q).
+  Axiom lft_extract_out : ∀ `(nclose lftN ⊆ E) κ P, [†κ] ⊢ κ ∋ P ={E}=★ ▷ P.
   Axiom lft_extract_lft : ∀ κ P, κ ∋ P ⊢ lft κ.
 
   (** Fractured borrows  *)
   (* TODO : I think an arbitrary mask is ok here. Not sure. *)
-  Axiom lft_borrow_fracture : ∀ E κ φ, &{κ}(φ 1%Qp) ={E}=> &frac{κ}φ.
+  Axiom lft_borrow_fracture : ∀ E κ φ, &{κ}(φ 1%Qp) ={E}=★ &frac{κ}φ.
   Axiom lft_frac_borrow_open : ∀ `(nclose lftN ⊆ E) κ φ q,
       □ (∀ q1 q2, φ (q1+q2)%Qp ↔ φ q1 ★ φ q2) ⊢
      &frac{κ}φ -★ [κ]{q} ={E}=★ ∃ q', ▷ φ q' ★ (▷ φ q' ={E}=★ [κ]{q}).
@@ -147,7 +146,7 @@ Section lft.
                                      lft_pers_borrow_own i κ'.
   Axiom lft_pers_borrow_open :
     ∀ `(nclose lftN ⊆ E) κ i P q,
-      lft_pers_borrow κ i P ⊢ lft_pers_borrow_own i κ ★ [κ]{q} ={E}=> ▷ P ★
+      lft_pers_borrow κ i P ⊢ lft_pers_borrow_own i κ ★ [κ]{q} ={E}=★ ▷ P ★
                                  (▷ P ={E}=★ lft_pers_borrow_own i κ ★ [κ]{q}).
   Axiom lft_pers_borrow_lft : ∀ κ i P, lft_pers_borrow κ i P ⊢ lft κ.
 
@@ -164,16 +163,16 @@ Section lft.
     nclose lftN ⊆ E →
       &{κ}P ⊢ [κ]{q} ={E}=★ ▷ P ★ (▷ P ={E}=★ &{κ}P ★ [κ]{q}).
   Proof.
-    iIntros (?) "HP Htok". iVs (lft_borrow_open with "HP Htok") as "[HP Hopen]". done.
-    iIntros "!==> {$HP} HP". by iApply (lft_borrow_close with "HP Hopen").
+    iIntros (?) "HP Htok". iMod (lft_borrow_open with "HP Htok") as "[HP Hopen]". done.
+    iIntros "!> {$HP} HP". by iApply (lft_borrow_close with "HP Hopen").
   Qed.
 
   Lemma lft_mkincl' E κ κ' q :
     nclose lftN ⊆ E →
-    lft κ ★ lft κ' ⊢ [κ]{q} ={E}=> κ' ⊑ κ ★ κ' ∋ [κ]{q}.
+    lft κ ★ lft κ' ⊢ [κ]{q} ={E}=★ κ' ⊑ κ ★ κ' ∋ [κ]{q}.
   Proof.
-    iIntros (?) "[#Hκ#Hκ']!#?".
-    iVs (lft_borrow_create with "Hκ' [-]") as "[??]". done. by iFrame.
+    iIntros (?) "[#Hκ#Hκ']?".
+    iMod (lft_borrow_create with "Hκ' [-]") as "[??]". done. by iFrame.
     iFrame. by iApply (lft_mkincl with "Hκ [-]").
   Qed.
 
@@ -182,7 +181,7 @@ Section lft.
       ={E}=★ &{κ}Q ★ [κ]{q}.
   Proof.
     iIntros "HP Hob Hvs".
-    iVs (lft_open_borrow_contravar with "Hob Hvs"). set_solver.
+    iMod (lft_open_borrow_contravar with "Hob Hvs"). set_solver.
     iApply (lft_borrow_close with "HP [-]"). set_solver. done.
   Qed.
 
@@ -192,24 +191,24 @@ Section lft.
     &{κ}(∃ x, Φ x) ⊢ [κ]{q} ={E}=★ ∃ x, &{κ}Φ x ★ [κ]{q}.
   Proof.
     iIntros "Hb Htok".
-    iVs (lft_borrow_open with "Hb Htok") as "[HΦ Hob]". done.
+    iMod (lft_borrow_open with "Hb Htok") as "[HΦ Hob]". done.
     iDestruct "HΦ" as (x) "HΦ".
-    iVs (lft_borrow_close_stronger with "HΦ Hob [-]") as "[Hown $]"; eauto 10.
+    iMod (lft_borrow_close_stronger with "HΦ Hob [-]") as "[Hown $]"; eauto 10.
   Qed.
 
   Lemma lft_borrow_or `{Inhabited A} `(nclose lftN ⊆ E) κ P Q q:
     &{κ}(P ∨ Q) ⊢ [κ]{q} ={E}=★ (&{κ}P ∨ &{κ}Q) ★ [κ]{q}.
   Proof.
     iIntros "H Htok". rewrite uPred.or_alt.
-    iVs (lft_borrow_exists with "H Htok") as ([]) "[H $]"; auto.
+    iMod (lft_borrow_exists with "H Htok") as ([]) "[H $]"; auto.
   Qed.
 
   Lemma lft_borrow_persistent `(nclose lftN ⊆ E) P {_:PersistentP P} κ q:
     &{κ}P ⊢ [κ]{q} ={E}=★ ▷ P ★ [κ]{q}.
   Proof.
     iIntros "Hb Htok".
-    iVs (lft_borrow_open with "Hb Htok") as "[#HP Hob]". done.
-    iVs (lft_borrow_close_stronger with "HP Hob [-]") as "[Hown $]"; eauto.
+    iMod (lft_borrow_open with "Hb Htok") as "[#HP Hob]". done.
+    iMod (lft_borrow_close_stronger with "HP Hob [-]") as "[Hown $]"; eauto.
   Qed.
 
 End lft.
@@ -235,25 +234,25 @@ Section shared_borrows.
   Global Instance lft_shr_borrow_persistent : PersistentP (&shr{κ | N} P) := _.
 
   Lemma lft_borrow_share E :
-    lftN ⊥ N → &{κ}P ={E}=> &shr{κ|N}P.
+    lftN ⊥ N → &{κ}P ={E}=★ &shr{κ|N}P.
   Proof.
     iIntros (?) "HP".
     iDestruct (lft_borrow_persist with "HP") as (κ' i) "(#?&#?&Hown)".
-    iExists κ', i. iVs (inv_alloc N E with "[Hown]").
+    iExists κ', i. iMod (inv_alloc N E with "[Hown]").
     by iIntros "!>"; iApply "Hown". by auto.
   Qed.
 
   Lemma lft_shr_borrow_open E q :
     nclose N ⊆ E → nclose lftN ⊆ E →
-    &shr{κ|N}P ⊢ [κ]{q} ={E,E∖N}=> ▷P ★ (▷P ={E∖N,E}=★ [κ]{q}).
+    &shr{κ|N}P ⊢ [κ]{q} ={E,E∖N}=★ ▷P ★ (▷P ={E∖N,E}=★ [κ]{q}).
   Proof.
-    iIntros (??) "#HP!#Hκ".
+    iIntros (??) "#HP Hκ".
     iDestruct "HP" as (κ' i) "(#Hord&%&#Hpers&#Hinv)". iInv N as ">Hown" "Hclose".
-    iVs (lft_incl_trade with "Hord Hκ") as (q') "(Hκ'&Hclose')". solve_ndisj.
-    iVs (lft_pers_borrow_open with "Hpers [Hown Hκ']") as "[HP Hclose'']".
+    iMod (lft_incl_trade with "Hord Hκ") as (q') "(Hκ'&Hclose')". solve_ndisj.
+    iMod (lft_pers_borrow_open with "Hpers [Hown Hκ']") as "[HP Hclose'']".
       solve_ndisj. by iFrame.
-    iIntros "{$HP}!==>HP". iVs ("Hclose''" with "HP") as "[Hown Hκ]".
-    iVs ("Hclose'" with "Hκ"). iFrame. iApply "Hclose". auto.
+    iIntros "{$HP}!>HP". iMod ("Hclose''" with "HP") as "[Hown Hκ]".
+    iMod ("Hclose'" with "Hκ"). iFrame. iApply "Hclose". auto.
   Qed.
 
   Lemma lft_shr_borrow_incl κ' :
@@ -295,27 +294,27 @@ Section tl_borrows.
   Qed.
 
   Lemma lft_borrow_share_tl E :
-    lftN ⊥ N → &{κ}P ={E}=> &tl{κ|tid|N}P.
+    lftN ⊥ N → &{κ}P ={E}=★ &tl{κ|tid|N}P.
   Proof.
     iIntros (?) "HP".
     iDestruct (lft_borrow_persist with "HP") as (κ' i) "(#?&#?&Hown)".
-    iExists κ', i. iVs (tl_inv_alloc tid E N with "[Hown]").
+    iExists κ', i. iMod (tl_inv_alloc tid E N with "[Hown]").
       by iIntros "!>"; iApply "Hown". by auto.
   Qed.
 
   Lemma lft_tl_borrow_open E F q :
     nclose lftN ⊆ E → nclose tlN ⊆ E → nclose N ⊆ F →
-    &tl{κ|tid|N}P ⊢ [κ]{q} ★ tl_own tid F ={E}=> ▷P ★ tl_own tid (F ∖ N) ★
+    &tl{κ|tid|N}P ⊢ [κ]{q} ★ tl_own tid F ={E}=★ ▷P ★ tl_own tid (F ∖ N) ★
                      (▷P ★ tl_own tid (F ∖ N) ={E}=★ [κ]{q} ★ tl_own tid F).
   Proof.
-    iIntros (???) "#HP!#[Hκ Htlown]".
+    iIntros (???) "#HP[Hκ Htlown]".
     iDestruct "HP" as (κ' i) "(#Hord&%&#Hpers&#Hinv)".
-    iVs (tl_inv_open with "Hinv Htlown") as "(>Hown&Htlown&Hclose)"; try done.
-    iVs (lft_incl_trade with "Hord Hκ") as (q') "(Hκ'&Hclose')". done.
-    iVs (lft_pers_borrow_open with "Hpers [Hown Hκ']") as "[HP Hclose'']".
+    iMod (tl_inv_open with "Hinv Htlown") as "(>Hown&Htlown&Hclose)"; try done.
+    iMod (lft_incl_trade with "Hord Hκ") as (q') "(Hκ'&Hclose')". done.
+    iMod (lft_pers_borrow_open with "Hpers [Hown Hκ']") as "[HP Hclose'']".
       done. by iFrame.
-    iIntros "{$HP $Htlown}!==>[HP Htlown]".
-    iVs ("Hclose''" with "HP") as "[Hown Hκ]". iVs ("Hclose'" with "Hκ").
+    iIntros "{$HP $Htlown}!>[HP Htlown]".
+    iMod ("Hclose''" with "HP") as "[Hown Hκ]". iMod ("Hclose'" with "Hκ").
     iFrame. iApply "Hclose". by iFrame.
   Qed.
 
diff --git a/lifting.v b/lifting.v
index e6d8d180fc56d8a8a8c46506b744e7b49186d5c6..80522fa241b44908a3a43e5791b12f37d77865a4 100644
--- a/lifting.v
+++ b/lifting.v
@@ -75,7 +75,7 @@ Lemma wp_read_na1_pst E l Φ :
   ⊢ WP Read Na1Ord (Lit $ LitLoc l) @ E {{ Φ }}.
 Proof.
   iIntros "HΦP". iApply (wp_lift_head_step E); auto.
-  iVs "HΦP" as (σ n v) "(%&HΦ&HP)". iVsIntro. iExists σ. iSplit. done. iFrame.
+  iMod "HΦP" as (σ n v) "(%&HΦ&HP)". iModIntro. iExists σ. iSplit. done. iFrame.
   iNext. iIntros (e2 σ2 ef) "[% HΦ]". inv_head_step.
   rewrite big_sepL_nil right_id. iApply ("HP" with "HΦ").
 Qed.
@@ -106,7 +106,7 @@ Lemma wp_write_na1_pst E l v Φ :
   ⊢ WP Write Na1Ord (Lit $ LitLoc l) (of_val v) @ E {{ Φ }}.
 Proof.
   iIntros "HΦP". iApply (wp_lift_head_step E); auto.
-  iVs "HΦP" as (σ v') "(%&HΦ&HP)". iVsIntro. iExists σ. iSplit. done. iFrame.
+  iMod "HΦP" as (σ v') "(%&HΦ&HP)". iModIntro. iExists σ. iSplit. done. iFrame.
   iNext. iIntros (e2 σ2 ef) "[% HΦ]". inv_head_step.
   rewrite big_sepL_nil right_id. iApply ("HP" with "HΦ").
 Qed.
@@ -162,7 +162,7 @@ Lemma wp_bin_op E op l1 l2 l' Φ :
 Proof.
   iIntros (?) "H". iApply wp_lift_pure_det_head_step; eauto.
   by intros; inv_head_step; eauto.
-  iNext. rewrite big_sepL_nil right_id. iVs "H". by iApply wp_value.
+  iNext. rewrite big_sepL_nil right_id. iMod "H". by iApply wp_value.
 Qed.
 
 Lemma wp_case E i e el Φ :
diff --git a/perm_incl.v b/perm_incl.v
index 28eb5a24973211e3b6aa73ab080d218a88abfca9..035e1d8655c49c05a58d6291ad42c3637e4dac69 100644
--- a/perm_incl.v
+++ b/perm_incl.v
@@ -1,5 +1,5 @@
 From Coq Require Import Qcanon.
-From iris.algebra Require Import upred_big_op.
+From iris.base_logic Require Import big_op.
 From iris.program_logic Require Import thread_local.
 From lrust Require Export type perm.
 
@@ -11,7 +11,7 @@ Section defs.
 
   (* Definitions *)
   Definition perm_incl (ρ1 ρ2 : perm) :=
-    ∀ tid, ρ1 tid ={⊤}=> ρ2 tid.
+    ∀ tid, ρ1 tid ={⊤}=★ ρ2 tid.
 
   Global Instance perm_equiv : Equiv perm :=
     λ ρ1 ρ2, perm_incl ρ1 ρ2 ∧ perm_incl ρ2 ρ1.
@@ -37,7 +37,7 @@ Section props.
   Proof.
     split.
     - iIntros (? tid) "H". eauto.
-    - iIntros (??? H12 H23 tid) "H". iVs (H12 with "H") as "H". by iApply H23.
+    - iIntros (??? H12 H23 tid) "H". iMod (H12 with "H") as "H". by iApply H23.
   Qed.
 
   Global Instance perm_equiv_equiv : Equivalence (⇔).
@@ -56,8 +56,8 @@ Section props.
     Proper ((⇔) ==> (⇔) ==> (⇔)) (sep).
   Proof.
     intros ??[A B]??[C D]; split; iIntros (tid) "[A B]".
-    iVs (A with "A") as "$". iApply (C with "B").
-    iVs (B with "A") as "$". iApply (D with "B").
+    iMod (A with "A") as "$". iApply (C with "B").
+    iMod (B with "A") as "$". iApply (D with "B").
   Qed.
 
   Lemma uPred_equiv_perm_equiv ρ θ : (∀ tid, ρ tid ⊣⊢ θ tid) → (ρ ⇔ θ).
@@ -74,7 +74,7 @@ Section props.
   Proof. iIntros (Hρ tid) "[?$]". by iApply Hρ. Qed.
 
   Lemma perm_incl_exists_intro {A} P x : P x ⇒ ∃ x : A, P x.
-  Proof. iIntros (tid) "H!==>". by iExists x. Qed.
+  Proof. iIntros (tid) "H!>". by iExists x. Qed.
 
   Global Instance perm_sep_assoc : Assoc (⇔) sep.
   Proof. intros ???; split. by iIntros (tid) "[$[$$]]". by iIntros (tid) "[[$$]$]". Qed.
@@ -89,28 +89,28 @@ Section props.
   Proof. intros ρ. by rewrite comm right_id. Qed.
 
   Lemma perm_incl_duplicable ρ (_ : Duplicable ρ) : ρ ⇒ ρ ★ ρ.
-  Proof. iIntros (tid) "#H!==>". by iSplit. Qed.
+  Proof. iIntros (tid) "#H!>". by iSplit. Qed.
 
   Lemma perm_tok_plus κ q1 q2 :
     tok κ q1 ★ tok κ q2 ⇔ tok κ (q1 + q2).
   Proof.
     rewrite /tok /sep /=; split; intros tid; rewrite -lft_own_op;
-      iIntros "[[$$]H]!==>". by iDestruct "H" as "[$?]". by auto.
+      iIntros "[[$$]H]!>". by iDestruct "H" as "[$?]". by auto.
   Qed.
 
   Lemma perm_lftincl_refl κ : ⊤ ⇒ κ ⊑ κ.
-  Proof. iIntros (tid) "_!==>". iApply lft_incl_refl. Qed.
+  Proof. iIntros (tid) "_!>". iApply lft_incl_refl. Qed.
 
   Lemma perm_lftincl_trans κ1 κ2 κ3 : κ1 ⊑ κ2 ★ κ2 ⊑ κ3 ⇒ κ1 ⊑ κ3.
-  Proof. iIntros (tid) "[#?#?]!==>". iApply lft_incl_trans. auto. Qed.
+  Proof. iIntros (tid) "[#?#?]!>". iApply lft_incl_trans. auto. Qed.
 
   Lemma perm_incl_share q v κ ty :
     v ◁ &uniq{κ} ty ★ [κ]{q} ⇒ v ◁ &shr{κ} ty ★ [κ]{q}.
   Proof.
     iIntros (tid) "[Huniq [Htok Hlft]]". destruct v; last by iDestruct "Huniq" as "[]".
     iDestruct "Huniq" as (l) "[% Hown]".
-    iVs (ty.(ty_share) _ lrustN with "Hown Htok") as "[Hown Htok]".
-    apply disjoint_union_l; solve_ndisj. set_solver. iVsIntro.
+    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.
   Qed.
 
@@ -189,8 +189,8 @@ Section props.
     rewrite split_prod_mt.
     iInduction (combine_offs tyl 0) as [|[ty offs] ll] "IH". by auto.
     rewrite big_sepL_cons /=.
-    iVs (lft_borrow_split with "H") as "[H0 H]". set_solver.
-    iVs ("IH" with "H") as "$". iVsIntro. iExists _. eauto.
+    iMod (lft_borrow_split with "H") as "[H0 H]". set_solver.
+    iMod ("IH" with "H") as "$". iModIntro. iExists _. eauto.
   Qed.
 
   Lemma perm_split_shr_borrow_prod tyl κ v :
@@ -203,7 +203,7 @@ Section props.
     destruct v as [[[|l|]|]|];
       iIntros "H"; try iDestruct "H" as "[]";
         iDestruct "H" as (l0) "[EQ H]"; iDestruct "EQ" as %[=]. subst l0.
-    simpl. iVsIntro.
+    simpl. iModIntro.
     change (ndot (A:=nat)) with (λ N i, N .@ (0+i)%nat).
     generalize O at 2; intro i.
     iInduction (combine_offs tyl 0) as [|[ty offs] ll] "IH" forall (i). by auto.
@@ -217,7 +217,7 @@ Section props.
     borrowing κ ρ ρ1 ρ2 → ρ ★ κ ∋ θ ★ ρ1 ⇒ ρ2 ★ κ ∋ (θ ★ ρ1).
   Proof.
     iIntros (Hbor tid) "(Hρ&Hθ&Hρ1)".
-    iVs (Hbor with "[#] Hρ Hρ1") as "[$ ?]". by iApply lft_extract_lft.
+    iMod (Hbor with "[#] Hρ Hρ1") as "[$ ?]". by iApply lft_extract_lft.
     iApply lft_extract_combine. set_solver. by iFrame.
   Qed.
 
@@ -228,11 +228,11 @@ Section props.
     destruct v as [[[|l|]|]|];
       try by (iDestruct "Hown" as "[]" || iDestruct "Hown" as (l) "[% _]").
     iDestruct "Hown" as (l') "[EQ [Hf Hown]]". iDestruct "EQ" as %[=]. subst l'.
-    iVs (lft_borrow_create with "Hκ Hown") as "[Hbor Hextract]". done.
+    iMod (lft_borrow_create with "Hκ Hown") as "[Hbor Hextract]". done.
     iSplitL "Hbor". by simpl; eauto.
-    iVs (lft_borrow_create with "Hκ Hf") as "[_ Hf]". done.
-    iVs (lft_extract_combine with "[-]"). done. by iFrame.
-    iVsIntro. iApply lft_extract_mono; last done.
+    iMod (lft_borrow_create with "Hκ Hf") as "[_ Hf]". done.
+    iMod (lft_extract_combine with "[-]"). done. by iFrame.
+    iModIntro. iApply lft_extract_mono; last done.
     iIntros "H/=". iExists _. iSplit. done. by iDestruct "H" as "[$$]".
   Qed.
 
@@ -243,8 +243,8 @@ Section props.
     destruct v as [[[|l|]|]|];
       try by (iDestruct "H" as "[]" || iDestruct "H" as (l) "[% _]").
     iDestruct "H" as (l') "[EQ H]". iDestruct "EQ" as %[=]. subst l'.
-    iVs (lft_reborrow with "Hord H") as "[H Hextr]". done.
-    iVsIntro. iSplitL "H". iExists _. by eauto.
+    iMod (lft_reborrow with "Hord H") as "[H Hextr]". done.
+    iModIntro. iSplitL "H". iExists _. by eauto.
     iApply (lft_extract_proper with "Hextr").
     iSplit; iIntros "H/=".
     - iDestruct "H" as (l') "[EQ H]". iDestruct "EQ" as %[=]. by subst l'.
@@ -258,15 +258,15 @@ Section props.
     destruct v as [[[|l|]|]|];
       try by (iDestruct "Hκ'" as "[]" || iDestruct "Hκ'" as (l) "[% _]").
     iDestruct "Hκ'" as (l') "[EQ Hκ']". iDestruct "EQ" as %[=]. subst l'.
-    iVsIntro. iExists _. iSplit. done.
+    iModIntro. iExists _. iSplit. done.
     by iApply (ty_shr_mono with "Hord Hκ'").
   Qed.
 
   Lemma lftincl_borrowing κ κ' q : borrowing κ ⊤ [κ']{q} (κ ⊑ κ').
   Proof.
     iIntros (tid) "#Hκ #Hord [Htok #Hκ']".
-    iVs (lft_mkincl' with "[#] Htok") as "[$ H]". done. by iFrame "#".
-    iVs (lft_borrow_create with "Hκ []") as "[_ H']". done. by iNext; iApply "Hκ'".
+    iMod (lft_mkincl' with "[#] Htok") as "[$ H]". done. by iFrame "#".
+    iMod (lft_borrow_create with "Hκ []") as "[_ H']". done. by iNext; iApply "Hκ'".
     iApply lft_extract_combine. done. by iFrame.
   Qed.
 
diff --git a/type.v b/type.v
index cc91ccccd7f6c05c0b244c4f41a569a0749b33f2..3f0fc938e8e140f534a3fd393003fca5990cc80a 100644
--- a/type.v
+++ b/type.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Import upred_big_op.
+From iris.base_logic Require Import big_op.
 From iris.program_logic Require Import hoare thread_local.
 From lrust Require Export notation lifetime heap.
 
@@ -38,7 +38,7 @@ Record type `{heapG Σ, lifetimeG Σ, thread_localG Σ} :=
     ty_shr_acc κ tid N E l q :
       nclose N ⊆ E → mgmtE ⊆ E → ty_dup →
       ty_shr κ tid N l ⊢
-        [κ]{q} ★ tl_own tid N ={E}=> ∃ q', ▷l ↦★{q'}: ty_own tid ★
+        [κ]{q} ★ tl_own tid N ={E}=★ ∃ q', ▷l ↦★{q'}: ty_own tid ★
            (▷l ↦★{q'}: ty_own tid ={E}=★ [κ]{q} ★ tl_own tid N)
   }.
 Global Existing Instances ty_shr_persistent ty_dup_persistent.
@@ -65,9 +65,9 @@ Program Coercion ty_of_st `{heapG Σ, lifetimeG Σ, thread_localG Σ}
 Next Obligation. intros. apply st_size_eq. Qed.
 Next Obligation.
   intros Σ ??? st E N κ l tid q ??. iIntros "Hmt Htok".
-  iVs (lft_borrow_exists with "Hmt Htok") as (vl) "[Hmt Htok]". set_solver.
-  iVs (lft_borrow_split with "Hmt") as "[Hmt Hown]". set_solver.
-  iVs (lft_borrow_persistent with "Hown Htok") as "[Hown $]". set_solver.
+  iMod (lft_borrow_exists with "Hmt Htok") as (vl) "[Hmt Htok]". set_solver.
+  iMod (lft_borrow_split with "Hmt") as "[Hmt Hown]". set_solver.
+  iMod (lft_borrow_persistent with "Hown Htok") as "[Hown $]". set_solver.
   iExists vl. iFrame. by iApply lft_borrow_fracture.
 Qed.
 Next Obligation.
@@ -76,13 +76,13 @@ 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]".
-  iVs (lft_frac_borrow_open with "[] Hf Hlft") as (q') "[Hmt Hclose]";
+  iMod (lft_frac_borrow_open with "[] Hf Hlft") as (q') "[Hmt Hclose]";
     first set_solver.
   - iIntros "!#". iIntros (q1 q2). rewrite heap_mapsto_vec_op_eq.
     iSplit; auto.
-  - iVsIntro. rewrite {1}heap_mapsto_vec_op_split. iExists _.
+  - iModIntro. rewrite {1}heap_mapsto_vec_op_split. iExists _.
     iDestruct "Hmt" as "[Hmt1 Hmt2]". iSplitL "Hmt1".
     + iNext. iExists _. by iFrame.
     + iIntros "Hmt1". iDestruct "Hmt1" as (vl') "[Hmt1 #Hown']".
@@ -111,9 +111,9 @@ Section types.
   Next Obligation. iIntros (tid vl) "[]". Qed.
   Next Obligation.
     iIntros (????????) "Hb Htok".
-    iVs (lft_borrow_exists with "Hb Htok") as (vl) "[Hb Htok]". set_solver.
-    iVs (lft_borrow_split with "Hb") as "[_ Hb]". set_solver.
-    iVs (lft_borrow_persistent with "Hb Htok") as "[>[] _]". set_solver.
+    iMod (lft_borrow_exists with "Hb Htok") as (vl) "[Hb Htok]". set_solver.
+    iMod (lft_borrow_split with "Hb") as "[_ Hb]". set_solver.
+    iMod (lft_borrow_persistent with "Hb Htok") as "[>[] _]". set_solver.
   Qed.
   Next Obligation. iIntros (?????) "_ []". Qed.
   Next Obligation. intros. iIntros "[]". Qed.
@@ -145,7 +145,7 @@ Section types.
                                ★ ▷ l ↦★: ty.(ty_own) tid)%I;
        ty_shr κ tid N l :=
          (∃ l':loc, &frac{κ}(λ q', l ↦{q'} #l') ★
-            ∀ q', [κ]{q'} ={mgmtE ∪ N, mgmtE}▷=> ty.(ty_shr) κ tid N l' ★ [κ]{q'})%I
+            ∀ q', □ ([κ]{q'} ={mgmtE ∪ N, mgmtE}▷=★ ty.(ty_shr) κ tid N l' ★ [κ]{q'}))%I
     |}.
   Next Obligation. done. Qed.
   Next Obligation.
@@ -153,39 +153,39 @@ Section types.
   Qed.
   Next Obligation.
     intros q ty E N κ l tid q' ?? =>/=. iIntros "Hshr Htok".
-    iVs (lft_borrow_exists with "Hshr Htok") as (vl) "[Hb Htok]". set_solver.
-    iVs (lft_borrow_split with "Hb") as "[Hb1 Hb2]". set_solver.
-    iVs (lft_borrow_exists with "Hb2 Htok") as (l') "[Hb2 Htok]". set_solver.
-    iVs (lft_borrow_split with "Hb2") as "[EQ Hb2]". set_solver.
-    iVs (lft_borrow_persistent with "EQ Htok") as "[>% Htok]". set_solver. subst.
+    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.
+    iMod (lft_borrow_split with "Hb2") as "[EQ Hb2]". set_solver.
+    iMod (lft_borrow_persistent with "EQ Htok") as "[>% Htok]". set_solver. subst.
     rewrite heap_mapsto_vec_singleton.
-    iVs (lft_borrow_split with "Hb2") as "[_ Hb2]". set_solver.
-    iVs (lft_borrow_fracture _ _ (λ q, l ↦{q} #l')%I with "Hb1") as "Hbf".
+    iMod (lft_borrow_split with "Hb2") as "[_ Hb2]". set_solver.
+    iMod (lft_borrow_fracture _ _ (λ q, l ↦{q} #l')%I with "Hb1") as "Hbf".
     rewrite lft_borrow_persist. iDestruct "Hb2" as (κ0 i) "(#Hord&#Hpb&Hpbown)".
-    iVs (inv_alloc N _ (lft_pers_borrow_own i κ0 ∨ ty_shr ty κ tid N l')%I
+    iMod (inv_alloc N _ (lft_pers_borrow_own i κ0 ∨ ty_shr ty κ tid N l')%I
          with "[Hpbown]") as "#Hinv"; first by eauto.
-    iIntros "!==>{$Htok}". iExists l'. iFrame. iIntros (q'') "!#Htok".
-    iVs (inv_open with "Hinv") as "[INV Hclose]". set_solver.
+    iIntros "!>{$Htok}". iExists l'. iFrame. iIntros (q'') "!#Htok".
+    iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
     replace ((mgmtE ∪ N) ∖ N) with mgmtE by set_solver.
     iDestruct "INV" as "[>Hbtok|#Hshr]".
     - iAssert (&{κ}▷ l' ↦★: ty_own ty tid)%I with "[Hbtok]" as "Hb".
       { iApply lft_borrow_persist. eauto. }
-      iVs (lft_borrow_open with "Hb Htok") as "[Hown Hob]". set_solver.
-      iIntros "!==>!>".
-      iVs (lft_borrow_close_stronger with "Hown Hob []") as "[Hb Htok]".
+      iMod (lft_borrow_open with "Hb Htok") as "[Hown Hob]". set_solver.
+      iIntros "!>". iNext.
+      iMod (lft_borrow_close_stronger with "Hown Hob []") as "[Hb Htok]".
         set_solver. eauto 10.
-      iVs (ty.(ty_share) with "Hb Htok") as "[#Hshr Htok]"; try done.
-      iVs ("Hclose" with "[]") as "_"; by eauto.
-    - iIntros "!==>!>". iVs ("Hclose" with "[]") as "_"; by eauto.
+      iMod (ty.(ty_share) with "Hb Htok") as "[#Hshr Htok]"; try done.
+      iMod ("Hclose" with "[]") as "_"; by eauto.
+    - iIntros "!>". iNext. iMod ("Hclose" with "[]") as "_"; by eauto.
   Qed.
   Next Obligation.
     iIntros (_ ty κ κ' tid N l) "#Hκ #H". iDestruct "H" as (l') "[Hfb Hvs]".
     iExists l'. iSplit. by iApply (lft_frac_borrow_incl with "[]").
     iIntros (q') "!#Htok".
-    iVs (lft_incl_trade with "Hκ Htok") as (q'') "[Htok Hclose]". set_solver.
-    iVs ("Hvs" $! q'' with "Htok") as "Hvs'".
-    iIntros "!==>!>". iVs "Hvs'" as "[Hshr Htok]".
-    iVs ("Hclose" with "Htok"). iFrame.
+    iMod (lft_incl_trade with "Hκ Htok") as (q'') "[Htok Hclose]". set_solver.
+    iMod ("Hvs" $! q'' with "Htok") as "Hvs'".
+    iIntros "!>". iNext. iMod "Hvs'" as "[Hshr Htok]".
+    iMod ("Hclose" with "Htok"). iFrame.
     by iApply (ty.(ty_shr_mono) with "Hκ").
   Qed.
   Next Obligation. done. Qed.
@@ -196,8 +196,8 @@ Section types.
          (∃ l:loc, vl = [ #l ] ★ &{κ} l ↦★: ty.(ty_own) tid)%I;
        ty_shr κ' tid N l :=
          (∃ l':loc, &frac{κ'}(λ q', l ↦{q'} #l') ★
-            ∀ q' κ'', κ'' ⊑ κ ★ κ'' ⊑ κ' ★ [κ'']{q'}
-               ={mgmtE ∪ N, mgmtE}▷=> ty.(ty_shr) κ'' tid N l' ★ [κ'']{q'})%I
+            ∀ q' κ'', □ (κ'' ⊑ κ ★ κ'' ⊑ κ' ★ [κ'']{q'}
+               ={mgmtE ∪ N, mgmtE}▷=★ ty.(ty_shr) κ'' tid N l' ★ [κ'']{q'}))%I
     |}.
   Next Obligation. done. Qed.
   Next Obligation.
@@ -205,30 +205,31 @@ Section types.
   Qed.
   Next Obligation.
     intros κ ty E N κ' l tid q' ?? =>/=. iIntros "Hshr Htok".
-    iVs (lft_borrow_exists with "Hshr Htok") as (vl) "[Hb Htok]". set_solver.
-    iVs (lft_borrow_split with "Hb") as "[Hb1 Hb2]". set_solver.
-    iVs (lft_borrow_exists with "Hb2 Htok") as (l') "[Hb2 Htok]". set_solver.
-    iVs (lft_borrow_split with "Hb2") as "[EQ Hb2]". set_solver.
-    iVs (lft_borrow_persistent with "EQ Htok") as "[>% Htok]". set_solver. subst.
+    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.
+    iMod (lft_borrow_split with "Hb2") as "[EQ Hb2]". set_solver.
+    iMod (lft_borrow_persistent with "EQ Htok") as "[>% Htok]". set_solver. subst.
     rewrite heap_mapsto_vec_singleton.
-    iVs (lft_borrow_fracture _ _ (λ q, l ↦{q} #l')%I with "Hb1") as "Hbf".
+    iMod (lft_borrow_fracture _ _ (λ q, l ↦{q} #l')%I with "Hb1") as "Hbf".
     rewrite lft_borrow_persist.
     iDestruct "Hb2" as (κ0 i) "(#Hord&#Hpb&Hpbown)".
-    iVs (inv_alloc N _ (lft_pers_borrow_own i κ0 ∨ ty_shr ty κ' tid N l')%I
+    iMod (inv_alloc N _ (lft_pers_borrow_own i κ0 ∨ ty_shr ty κ' tid N l')%I
          with "[Hpbown]") as "#Hinv"; first by eauto.
-    iIntros "!==>{$Htok}". iExists l'. iFrame.
+    iIntros "!>{$Htok}". iExists l'. iFrame.
     iIntros (q'' κ'') "!#(#Hκ''κ & #Hκ''κ' & Htok)".
-    iVs (inv_open with "Hinv") as "[INV Hclose]". set_solver.
+    iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
     replace ((mgmtE ∪ N) ∖ N) with mgmtE by set_solver.
     iDestruct "INV" as "[>Hbtok|#Hshr]".
     - iAssert (&{κ''}&{κ} l' ↦★: ty_own ty tid)%I with "[Hbtok]" as "Hb".
       { iApply lft_borrow_persist. iExists κ0, i. iFrame "★ #".
         iApply lft_incl_trans. eauto. }
-      iVs (lft_borrow_open with "Hb Htok") as "[Hown Hob]". set_solver.
-      iIntros "!==>!>".
-      iVs (lft_borrow_unnest with "Hκ''κ [Hown Hob]") as "[Htok Hb]". set_solver. by iFrame.
-      iVs (ty.(ty_share) with "Hb Htok") as "[#Hshr Htok]"; try done.
-      iVs ("Hclose" with "[]") as "_".
+      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 (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]
          does not work here, because we do not know at the beginning
          at which lifetime we will need the sharing.
@@ -237,17 +238,17 @@ Section types.
          need a lifetime that would be the union of κ and κ'. *)
       admit.
       by eauto.
-    - iIntros "!==>!>". iVs ("Hclose" with "[]") as "_". by eauto.
-      iIntros "!==>{$Htok}". by iApply (ty.(ty_shr_mono) with "Hκ''κ'").
+    - iIntros "!>". iNext. iMod ("Hclose" with "[]") as "_". by eauto.
+      iIntros "!>{$Htok}". by iApply (ty.(ty_shr_mono) with "Hκ''κ'").
   Admitted.
   Next Obligation.
     iIntros (κ0 ty κ κ' tid N l) "#Hκ #H". iDestruct "H" as (l') "[Hfb Hvs]".
     iExists l'. iSplit. by iApply (lft_frac_borrow_incl with "[]").
     iIntros (q' κ'') "!#(#Hκ0 & #Hκ' & Htok)".
-    iVs ("Hvs" $! q' κ'' with "[Htok]") as "Hclose".
+    iMod ("Hvs" $! q' κ'' with "[Htok]") as "Hclose".
     { iFrame. iSplit. done. iApply lft_incl_trans. eauto. }
-    iIntros "!==>!>". iVs "Hclose" as "[Hshr Htok]".
-    iIntros "!==>{$Htok}". iApply (ty.(ty_shr_mono) with "[] Hshr").
+    iIntros "!>". iNext. iMod "Hclose" as "[Hshr Htok]".
+    iIntros "!>{$Htok}". iApply (ty.(ty_shr_mono) with "[] Hshr").
     iApply lft_incl_refl.
   Qed.
   Next Obligation. done. Qed.
@@ -355,13 +356,13 @@ Section types.
     intros tyl E N κ l tid q ??. rewrite split_prod_mt.
     change (ndot (A:=nat)) with (λ N i, N .@ (0+i)%nat). generalize O at 3.
     induction (combine_offs tyl 0) as [|[ty offs] ll IH].
-    - iIntros (?) "_$!==>". by rewrite big_sepL_nil.
+    - iIntros (?) "_$!>". by rewrite big_sepL_nil.
     - iIntros (i) "Hown Htoks". rewrite big_sepL_cons.
-      iVs (lft_borrow_split with "Hown") as "[Hownh Hownq]". set_solver.
-      iVs (IH (S i)%nat with "Hownq Htoks") as "[#Hshrq Htoks]".
-      iVs (ty.(ty_share) _ (N .@ (i+0)%nat) with "Hownh Htoks") as "[#Hshrh $]".
+      iMod (lft_borrow_split with "Hown") as "[Hownh Hownq]". set_solver.
+      iMod (IH (S i)%nat with "Hownq Htoks") as "[#Hshrq Htoks]".
+      iMod (ty.(ty_share) _ (N .@ (i+0)%nat) with "Hownh Htoks") as "[#Hshrh $]".
         solve_ndisj. done.
-      iVsIntro. rewrite big_sepL_cons. iFrame "#".
+      iModIntro. rewrite big_sepL_cons. iFrame "#".
       iApply big_sepL_mono; last done. intros. by rewrite /= Nat.add_succ_r.
   Qed.
   Next Obligation.
@@ -375,16 +376,16 @@ Section types.
     destruct (split_prod_namespace tid N (length tyl)) as [Ef [EQ _]].
     setoid_rewrite ->EQ. clear EQ. generalize 0%nat.
     revert q. induction tyl as [|tyh tyq IH].
-    - iIntros (q i offs) "_!#$!==>". iExists 1%Qp. rewrite big_sepL_nil. auto.
+    - iIntros (q i offs) "_$!>". iExists 1%Qp. rewrite big_sepL_nil. auto.
     - simpl in DUP. destruct (andb_prop_elim _ _ DUP) as [DUPh DUPq]. simpl.
-      iIntros (q i offs) "#Hshr!#([Htokh Htokq]&Htlf&Htlh&Htlq)".
+      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.
-      iVs (IH with "Hshrq [Htokq Htlf Htlq]") as (q'q) "[Hownq Hcloseq]". by iFrame.
-      iVs (tyh.(ty_shr_acc) with "Hshrh [Htokh Htlh]") as (q'h) "[Hownh Hcloseh]"; try done.
+      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.
       destruct (Qp_lower_bound q'h q'q) as (q' & q'0h & q'0q & -> & ->).
-      iExists q'. iVsIntro. rewrite big_sepL_cons.
+      iExists q'. iModIntro. rewrite big_sepL_cons.
       rewrite -heap_mapsto_vec_prop_op; last apply ty_size_eq.
       iDestruct "Hownh" as "[Hownh0 Hownh1]".
       rewrite (big_sepL_proper (λ _ x, _ ↦★{_}: _)%I); last first.
@@ -393,8 +394,8 @@ Section types.
       rewrite big_sepL_sepL. iDestruct "Hownq" as "[Hownq0 Hownq1]".
       iSplitL "Hownh0 Hownq0". iNext. by iFrame.
       iIntros "[Hh Hq]". rewrite (lft_own_split κ q).
-      iVs ("Hcloseh" with "[Hh Hownh1]") as "($&$)". iNext. by iFrame.
-      iVs ("Hcloseq" with "[Hq Hownq1]") as "($&$&$)". iNext. by iFrame.
+      iMod ("Hcloseh" with "[Hh Hownh1]") as "($&$)". iNext. by iFrame.
+      iMod ("Hcloseq" with "[Hq Hownq1]") as "($&$&$)". iNext. by iFrame.
       done.
   Qed.
 
@@ -447,9 +448,9 @@ Section types.
   Qed.
   Next Obligation.
     intros n tyl Hn E N κ l tid q ??. iIntros "Hown Htok". rewrite split_sum_mt.
-    iVs (lft_borrow_exists with "Hown Htok") as (i) "[Hown Htok]". set_solver.
-    iVs (lft_borrow_split with "Hown") as "[Hmt Hown]". set_solver.
-    iVs ((nth i tyl emp).(ty_share) with "Hown Htok") as "[#Hshr Htok]"; try done.
+    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.
   Qed.
   Next Obligation.
@@ -460,16 +461,16 @@ Section types.
   Qed.
   Next Obligation.
     intros n tyl Hn κ tid N E l q ?? Hdup%Is_true_eq_true.
-    iIntros "#H!#[[Htok1 Htok2] Htl]".
+    iIntros "#H[[Htok1 Htok2] Htl]".
     setoid_rewrite split_sum_mt. iDestruct "H" as (i) "[Hshr0 Hshr]".
-    iVs (lft_frac_borrow_open with "[] Hshr0 Htok1") as (q'1) "[Hown Hclose]". set_solver.
+    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. }
-    iVs ((nth i tyl emp).(ty_shr_acc) with "Hshr [Htok2 Htl]")
+    iMod ((nth i tyl emp).(ty_shr_acc) with "Hshr [Htok2 Htl]")
       as (q'2) "[Hownq Hclose']"; try done; [|by iFrame|].
     { 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 & -> & ->).
-    iExists q'. iVsIntro.
+    iExists q'. iModIntro.
     rewrite -{1}heap_mapsto_op_eq -{1}heap_mapsto_vec_prop_op;
       last (by intros; apply sum_size_eq, Hn).
     iDestruct "Hownq" as "[Hownq1 Hownq2]". iDestruct "Hown" as "[Hown1 Hown2]".
@@ -479,7 +480,7 @@ Section types.
       rewrite (lft_own_split _ q).
       iCombine "Hown1" "Hown2" as "Hown". rewrite heap_mapsto_op.
       iDestruct "Hown" as "[>#Hi Hown]". iDestruct "Hi" as %[= ->%Z_of_nat_inj].
-      iVs ("Hclose" with "Hown") as "$".
+      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").
diff --git a/type_incl.v b/type_incl.v
index 7566f24797f2adc774ff72d70a93294ab46d1212..dd531378f48b8c162cc61d28757efe34f6191aaa 100644
--- a/type_incl.v
+++ b/type_incl.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Import upred_big_op.
+From iris.base_logic Require Import big_op.
 From iris.program_logic Require Import thread_local hoare.
 From lrust Require Export type perm_incl.
 
@@ -9,7 +9,7 @@ Section ty_incl.
   Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}.
 
   Definition ty_incl (ρ : perm) (ty1 ty2 : type) :=
-    ∀ tid, ρ tid ={⊤}=>
+    ∀ tid, ρ tid ={⊤}=★
       (□ ∀ vl, ty1.(ty_own) tid vl → ty2.(ty_own) tid vl) ★
       (□ ∀ κ E l, ty1.(ty_shr) κ tid E l →
        (* [ty_incl] needs to prove something about the length of the
@@ -19,15 +19,15 @@ Section ty_incl.
                   ty2.(ty_shr) κ tid E l ★ ty1.(ty_size) = ty2.(ty_size)).
 
   Global Instance ty_incl_refl ρ : Reflexive (ty_incl ρ).
-  Proof. iIntros (ty tid) "_!==>". iSplit; iIntros "!#"; eauto. Qed.
+  Proof. iIntros (ty tid) "_!>". iSplit; iIntros "!#"; eauto. Qed.
 
   Lemma ty_incl_trans ρ θ ty1 ty2 ty3 :
     ty_incl ρ ty1 ty2 → ty_incl θ ty2 ty3 → ty_incl (ρ ★ θ) ty1 ty3.
   Proof.
     iIntros (H12 H23 tid) "[H1 H2]".
-    iVs (H12 with "H1") as "[#H12 #H12']".
-    iVs (H23 with "H2") as "[#H23 #H23']".
-    iVsIntro; iSplit; iIntros "!#*H1".
+    iMod (H12 with "H1") as "[#H12 #H12']".
+    iMod (H23 with "H2") as "[#H23 #H23']".
+    iModIntro; iSplit; iIntros "!#*H1".
     - by iApply "H23"; iApply "H12".
     - iDestruct ("H12'" $! _ _ _ with "H1") as "[H2 %]".
       iDestruct ("H23'" $! _ _ _ with "H2") as "[$ %]".
@@ -36,7 +36,7 @@ Section ty_incl.
 
   Lemma ty_incl_weaken ρ θ ty1 ty2 :
     ρ ⇒ θ → ty_incl θ ty1 ty2 → ty_incl ρ ty1 ty2.
-  Proof. iIntros (Hρθ Hρ' tid) "H". iVs (Hρθ with "H"). by iApply Hρ'. Qed.
+  Proof. iIntros (Hρθ Hρ' tid) "H". iMod (Hρθ with "H"). by iApply Hρ'. Qed.
 
   Global Instance ty_incl_preorder ρ: Duplicable ρ → PreOrder (ty_incl ρ).
   Proof.
@@ -45,13 +45,13 @@ Section ty_incl.
   Qed.
 
   Lemma ty_incl_emp ρ ty : ty_incl ρ ! ty.
-  Proof. iIntros (tid) "_!==>". iSplit; iIntros "!#*/=[]". Qed.
+  Proof. iIntros (tid) "_!>". iSplit; iIntros "!#*/=[]". Qed.
 
   Lemma ty_incl_own ρ ty1 ty2 q :
     ty_incl ρ ty1 ty2 → ty_incl ρ (own q ty1) (own q ty2).
   Proof.
-    iIntros (Hincl tid) "H/=". iVs (Hincl with "H") as "[#Howni #Hshri]".
-    iVsIntro. iSplit; iIntros "!#*H".
+    iIntros (Hincl tid) "H/=". iMod (Hincl with "H") as "[#Howni #Hshri]".
+    iModIntro. iSplit; iIntros "!#*H".
     - iDestruct "H" as (l) "(%&H†&Hmt)". subst. iExists _. iSplit. done.
       iDestruct "Hmt" as (vl') "[Hmt Hown]". iNext.
       iDestruct (ty_size_eq with "Hown") as %<-.
@@ -60,15 +60,15 @@ Section ty_incl.
       iExists _. by iFrame.
     - iDestruct "H" as (l') "[Hfb #Hvs]". iSplit; last done. iExists l'. iFrame.
       iIntros (q') "!#Hκ".
-      iVs ("Hvs" $! _ with "Hκ") as "Hvs'". iIntros "!==>!>".
-      iVs "Hvs'" as "[Hshr $]". iVsIntro.
+      iMod ("Hvs" $! _ with "Hκ") as "Hvs'". iIntros "!>". iNext.
+      iMod "Hvs'" as "[Hshr $]". iModIntro.
       by iDestruct ("Hshri" $! _ _ _ with "Hshr") as "[$ _]".
   Qed.
 
   Lemma lft_incl_ty_incl_uniq_borrow ty κ1 κ2 :
     ty_incl (κ1 ⊑ κ2) (&uniq{κ2}ty) (&uniq{κ1}ty).
   Proof.
-    iIntros (tid) "#Hincl!==>". iSplit; iIntros "!#*H".
+    iIntros (tid) "#Hincl!>". iSplit; iIntros "!#*H".
     - iDestruct "H" as (l) "[% Hown]". subst. iExists _. iSplit. done.
       by iApply (lft_borrow_incl with "Hincl").
     - admit. (* TODO : fix the definition before *)
@@ -77,7 +77,7 @@ Section ty_incl.
   Lemma lft_incl_ty_incl_shared_borrow ty κ1 κ2 :
     ty_incl (κ1 ⊑ κ2) (&shr{κ2}ty) (&shr{κ1}ty).
   Proof.
-    iIntros (tid) "#Hincl!==>". iSplit; iIntros "!#*H".
+    iIntros (tid) "#Hincl!>". iSplit; iIntros "!#*H".
     - iDestruct "H" as (l) "[% Hown]". subst. iExists _. iSplit. done.
       by iApply (ty.(ty_shr_mono) with "Hincl").
     - iDestruct "H" as (vl) "#[Hfrac Hty]". iSplit; last done.
@@ -93,27 +93,27 @@ Section ty_incl.
     Duplicable ρ → Forall2 (ty_incl ρ) tyl1 tyl2 → ty_incl ρ (Π tyl1) (Π tyl2).
   Proof.
     intros Hρ HFA. iIntros (tid) "#Hρ". iSplitL "".
-    - assert (Himpl : ρ tid ={⊤}=>
+    - assert (Himpl : ρ tid ={⊤}=★
          □ (∀ vll, length tyl1 = length vll →
                ([★ list] tyvl ∈ combine tyl1 vll, ty_own (tyvl.1) tid (tyvl.2))
              → ([★ list] tyvl ∈ combine tyl2 vll, ty_own (tyvl.1) tid (tyvl.2)))).
       { induction HFA as [|ty1 ty2 tyl1 tyl2 Hincl HFA IH].
-        - iIntros "_!==>!#* _ _". by rewrite big_sepL_nil.
-        - iIntros "#Hρ". iVs (IH with "Hρ") as "#Hqimpl".
-          iVs (Hincl with "Hρ") as "[#Hhimpl _]".
-          iIntros "!==>!#*%". destruct vll as [|vlh vllq]. done.
+        - iIntros "_!>!#* _ _". by rewrite big_sepL_nil.
+        - iIntros "#Hρ". iMod (IH with "Hρ") as "#Hqimpl".
+          iMod (Hincl with "Hρ") as "[#Hhimpl _]".
+          iIntros "!>!#*%". destruct vll as [|vlh vllq]. done.
           rewrite !big_sepL_cons.
           iIntros "[Hh Hq]". iSplitL "Hh". by iApply "Hhimpl".
           iApply ("Hqimpl" with "[] Hq"). iPureIntro. simpl in *. congruence. }
-      iVs (Himpl with "Hρ") as "#Himpl". iIntros "!==>!#*H".
+      iMod (Himpl with "Hρ") as "#Himpl". iIntros "!>!#*H".
       iDestruct "H" as (vll) "(%&%&H)". iExists _. iSplit. done. iSplit.
       by rewrite -(Forall2_length _ _ _ HFA). by iApply ("Himpl" with "[] H").
     - rewrite /Π /=. iRevert "Hρ". generalize O; intros offs.
       change (ndot (A:=nat)) with (λ N i, N .@ (0+i)%nat). generalize O; intros i.
       iInduction HFA as [|ty1 ty2 tyl1 tyl2 Hincl HFA] "IH" forall (i offs).
-      + iIntros "_!==>!#*_/=". rewrite big_sepL_nil. eauto.
-      + iIntros "#Hρ". iVs ("IH" $! _ _ with "[]") as "#Hqimpl"; try done.
-        iVs (Hincl with "Hρ") as "[_ #Hhimpl]". iIntros "!==>!#*".
+      + iIntros "_!>!#*_/=". rewrite big_sepL_nil. eauto.
+      + iIntros "#Hρ". iMod ("IH" $! _ _ with "[]") as "#Hqimpl"; try done.
+        iMod (Hincl with "Hρ") as "[_ #Hhimpl]". iIntros "!>!#*".
         rewrite !big_sepL_cons. iIntros "[Hh Hq]".
         setoid_rewrite <-Nat.add_succ_comm.
         iDestruct ("Hhimpl" $! _ _ _ with "Hh") as "[$ %]".
@@ -125,7 +125,7 @@ Section ty_incl.
   Lemma ty_incl_prod_cons_l ρ ty tyl :
     ty_incl ρ (Π(ty :: tyl)) (Π[ty ; Π tyl]).
   Proof.
-    iIntros (tid) "_!==>". iSplit; iIntros "!#/=".
+    iIntros (tid) "_!>". iSplit; iIntros "!#/=".
     - iIntros (vl) "H". iDestruct "H" as ([|vlh vllq]) "(%&%&H)". done. subst.
       iExists [_;_]. iSplit. by rewrite /= app_nil_r. iSplit. done.
       rewrite !big_sepL_cons big_sepL_nil right_id. iDestruct "H" as "[$ H]".
@@ -147,33 +147,33 @@ Section ty_incl.
     ty_incl ρ (sum tyl1) (sum tyl2).
   Proof.
     iIntros (DUP FA tid) "#Hρ". rewrite /sum /=. iSplitR "".
-    - assert (Hincl : ρ tid ={⊤}=>
+    - assert (Hincl : ρ tid ={⊤}=★
          (□ ∀ i vl, (nth i tyl1 !%T).(ty_own) tid vl
                   → (nth i tyl2 !%T).(ty_own) tid vl)).
       { clear -FA DUP. induction FA as [|ty1 ty2 tyl1 tyl2 Hincl _ IH].
-        - iIntros "_!==>*!#". eauto.
-        - iIntros "#Hρ".  iVs (IH with "Hρ") as "#IH". iVs (Hincl with "Hρ") as "[#Hh _]".
-          iIntros "!==>*!#*Hown". destruct i as [|i]. by iApply "Hh". by iApply "IH". }
-      iVs (Hincl with "Hρ") as "#Hincl". iIntros "!==>!#*H".
+        - iIntros "_!>*!#". eauto.
+        - iIntros "#Hρ".  iMod (IH with "Hρ") as "#IH". iMod (Hincl with "Hρ") as "[#Hh _]".
+          iIntros "!>*!#*Hown". destruct i as [|i]. by iApply "Hh". by iApply "IH". }
+      iMod (Hincl with "Hρ") as "#Hincl". iIntros "!>!#*H".
       iDestruct "H" as (i vl') "[% Hown]". subst. iExists _, _. iSplit. done.
         by iApply "Hincl".
-    - assert (Hincl : ρ tid ={⊤}=>
+    - assert (Hincl : ρ tid ={⊤}=★
          (□ ∀ i κ E l, (nth i tyl1 !%T).(ty_shr) κ tid E l
                      → (nth i tyl2 !%T).(ty_shr) κ tid E l)).
       { clear -FA DUP. induction FA as [|ty1 ty2 tyl1 tyl2 Hincl _ IH].
-        - iIntros "_!==>*!#". eauto.
+        - iIntros "_!>*!#". eauto.
         - iIntros "#Hρ".
-          iVs (IH with "Hρ") as "#IH". iVs (Hincl with "Hρ") as "[_ #Hh]".
-          iIntros "!==>*!#*Hown". destruct i as [|i]; last by iApply "IH".
+          iMod (IH with "Hρ") as "#IH". iMod (Hincl with "Hρ") as "[_ #Hh]".
+          iIntros "!>*!#*Hown". destruct i as [|i]; last by iApply "IH".
           by iDestruct ("Hh" $! _ _ _ with "Hown") as "[$ _]". }
-      iVs (Hincl with "Hρ") as "#Hincl". iIntros "!==>!#*H". iSplit; last done.
+      iMod (Hincl with "Hρ") as "#Hincl". iIntros "!>!#*H". iSplit; last done.
       iDestruct "H" as (i) "[??]". iExists _. iSplit. done. by iApply "Hincl".
   Qed.
 
   Lemma ty_incl_uninit_split ρ n1 n2 :
     ty_incl ρ (uninit (n1+n2)) (Π[uninit n1; uninit n2]).
   Proof.
-    iIntros (tid) "_!==>". iSplit; iIntros "!#*H".
+    iIntros (tid) "_!>". iSplit; iIntros "!#*H".
     - iDestruct "H" as %Hlen. iExists [take n1 vl; drop n1 vl].
       repeat iSplit. by rewrite /= app_nil_r take_drop. done.
       rewrite big_sepL_cons big_sepL_singleton. iSplit; iPureIntro.
@@ -200,9 +200,9 @@ Section ty_incl.
     Duplicable ρ → (∀ vl : vec val n, ρ ★ ρ2 vl ⇒ ρ1 vl) →
     ty_incl ρ (cont ρ1) (cont ρ2).
   Proof.
-    iIntros (? Hρ1ρ2 tid) "#Hρ!==>". iSplit; iIntros "!#*H"; last by auto.
+    iIntros (? Hρ1ρ2 tid) "#Hρ!>". iSplit; iIntros "!#*H"; last by auto.
     iDestruct "H" as (f) "[% Hwp]". subst. iExists _. iSplit. done.
-    iIntros (vl) "Hρ2 Htl". iVs (Hρ1ρ2 with "[Hρ2]"). by iFrame.
+    iIntros (vl) "Hρ2 Htl". iMod (Hρ1ρ2 with "[Hρ2]"). by iFrame.
     by iApply ("Hwp" with "[-Htl] Htl").
   Qed.
 
@@ -210,21 +210,21 @@ Section ty_incl.
     Duplicable ρ → (∀ (x : A) (vl : vec val n), ρ ★ ρ2 x vl ⇒ ρ1 x vl) →
     ty_incl ρ (fn ρ1) (fn ρ2).
   Proof.
-    iIntros (? Hρ1ρ2 tid) "#Hρ!==>". iSplit; iIntros "!#*#H".
+    iIntros (? Hρ1ρ2 tid) "#Hρ!>". iSplit; iIntros "!#*#H".
     - iDestruct "H" as (f) "[% Hwp]". subst. iExists _. iSplit. done.
-      iIntros (x vl) "!#[Hρ2 Htl]". iVs (Hρ1ρ2 with "[Hρ2]"). by iFrame.
+      iIntros (x vl) "!#[Hρ2 Htl]". iMod (Hρ1ρ2 with "[Hρ2]"). by iFrame.
       iApply "Hwp". by iFrame.
     - iSplit; last done. simpl. iDestruct "H" as (vl0) "[? Hvl]".
       iExists vl0. iFrame "#". iNext. iDestruct "Hvl" as (f) "[% Hwp]".
       iExists f. iSplit. done.
-      iIntros (x vl) "!#[Hρ2 Htl]". iVs (Hρ1ρ2 with "[Hρ2]"). by iFrame.
+      iIntros (x vl) "!#[Hρ2 Htl]". iMod (Hρ1ρ2 with "[Hρ2]"). by iFrame.
       iApply "Hwp". by iFrame.
   Qed.
 
   Lemma ty_incl_fn_cont {A n} ρ ρf (x : A) :
     ty_incl ρ (fn ρf) (cont (n:=n) (ρf x)).
   Proof.
-    iIntros (tid) "_!==>". iSplit; iIntros "!#*H"; last by iSplit.
+    iIntros (tid) "_!>". iSplit; iIntros "!#*H"; last by iSplit.
     iDestruct "H" as (f) "[%#H]". subst. iExists _. iSplit. done.
     iIntros (vl) "Hρf Htl". iApply "H". by iFrame.
   Qed.
@@ -232,7 +232,7 @@ Section ty_incl.
   Lemma ty_incl_fn_specialize {A B n} (f : A → B) ρ ρfn :
     ty_incl ρ (fn (n:=n) ρfn) (fn (ρfn ∘ f)).
   Proof.
-    iIntros (tid) "_!==>". iSplit; iIntros "!#*H".
+    iIntros (tid) "_!>". iSplit; iIntros "!#*H".
     - iDestruct "H" as (fv) "[%#H]". subst. iExists _. iSplit. done.
       iIntros (x vl). by iApply "H".
     - iSplit; last done.
@@ -244,7 +244,7 @@ Section ty_incl.
   Lemma ty_incl_perm_incl ρ ty1 ty2 v :
     ty_incl ρ ty1 ty2 → ρ ★ v ◁ ty1 ⇒ v ◁ ty2.
   Proof.
-    iIntros (Hincl tid) "[Hρ Hty1]". iVs (Hincl with "Hρ") as "[#Hownincl _]".
+    iIntros (Hincl tid) "[Hρ Hty1]". iMod (Hincl with "Hρ") as "[#Hownincl _]".
     destruct v; last done. by iApply "Hownincl".
   Qed.
 
diff --git a/typing.v b/typing.v
index 764f23155b5cfd6bf1c8de707d8e5bceebd90f2e..117d8d6c7bf2097c1ec5a85952b5586f1d746291 100644
--- a/typing.v
+++ b/typing.v
@@ -133,9 +133,9 @@ Section typing.
   Lemma typed_step_newlft ρ:
     typed_step ρ Newlft (λ _, ∃ α, [α]{1} ★ α ∋ top)%P.
   Proof.
-    iIntros (tid) "_!#[_$]". wp_value. iVs lft_begin as (α) "[?#?]". done.
-    iVs (lft_borrow_create with "[][]") as "[_?]". done. done.
-    2:by iVsIntro; iExists α; iFrame. eauto.
+    iIntros (tid) "_!#[_$]". wp_value. iMod lft_begin as (α) "[?#?]". done.
+    iMod (lft_borrow_create with "[][]") as "[_?]". done. done.
+    2:by iModIntro; iExists α; iFrame. eauto.
   Qed.
 
   Lemma typed_step_endlft κ ρ:
@@ -146,14 +146,14 @@ Section typing.
     iApply (wp_wand_r _ _ (λ _, _ ★ True)%I). iSplitR "Hextr".
     iApply (wp_frame_step_l with "[-]"); try done.
     iDestruct (lft_end with "Hlft Htok") as "$". by wp_seq.
-    iIntros (v) "[#Hκ _]". iVs (lft_extract_out with "Hκ Hextr"). done.
+    iIntros (v) "[#Hκ _]". iMod (lft_extract_out with "Hκ Hextr"). done.
     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 "!==>".
+    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.
@@ -170,7 +170,7 @@ Section typing.
   Qed.
 
   Definition consumes (ty : type) (ρ1 ρ2 : Valuable.t → perm) : Prop :=
-    ∀ (l:loc) tid, ρ1 (Some #l) tid ★ tl_own tid ⊤ ={mgmtE ∪ lrustN}=>
+    ∀ (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 ⊤)).
@@ -185,7 +185,7 @@ Section typing.
     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↦!==>".
+    iModIntro. iExists _, _. iFrame "★#%". iIntros "!>!>!>H↦!>".
     iExists _. iSplit. done. iFrame. iExists vl. eauto.
   Qed.
 
@@ -196,7 +196,7 @@ Section typing.
     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↦!==>".
+    iModIntro. iExists _, _. iFrame "★#%". iIntros "!>!>!>H↦!>".
     iExists _. iSplit. done. iFrame. iExists vl. eauto.
   Qed.
 
@@ -207,7 +207,7 @@ Section typing.
     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↦!==>".
+    iModIntro. iExists _, _. iFrame "★#%". iIntros "!>!>!>H↦!>".
     iExists _. iSplit. done. iFrame. iExists vl. eauto.
   Qed.
 
diff --git a/wp_tactics.v b/wp_tactics.v
index df840ba7221647fb96906d36aeee9f512267296e..0775226d94c4be664d143af37e3941ff34253e64 100644
--- a/wp_tactics.v
+++ b/wp_tactics.v
@@ -1,4 +1,3 @@
-From iris.algebra Require Export upred_tactics.
 From lrust Require Export tactics derived.
 Import uPred.
 
@@ -26,11 +25,11 @@ pvs_intro if we obtain a consecutive wp *)
 Ltac wp_strip_pvs :=
   lazymatch goal with
   | |- _ ⊢ |={?E}=> _ =>
-    etrans; [|apply pvs_intro];
+    etrans; [|apply fupd_intro];
     match goal with |- _ ⊢ wp E _ _ => simpl | _ => fail end
   end.
 
-Ltac wp_value_head := etrans; [|eapply wp_value_pvs; wp_done]; lazy beta.
+Ltac wp_value_head := etrans; [|eapply wp_value_fupd; wp_done]; lazy beta.
 
 Ltac wp_strip_later := idtac. (* a hook to be redefined later *)