diff --git a/opam b/opam
index 510b3089a96d6d380250aaaae4f7968e73c115a8..aecd02cb410b304e1b8b1664234401254913f103 100644
--- a/opam
+++ b/opam
@@ -11,5 +11,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-iris" { (= "dev.2018-06-23.0.a6e581d0") | (= "dev") }
+  "coq-iris" { (= "branch.gen_proofmode.2018-05-28.0.daeeaf05") | (= "dev") }
 ]
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index fd04e13dd101e930522a8153cbe9cbf341b5ef17..94d49b2bf92e04a0084a747465dcf0b4d62d88cc 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -2,7 +2,7 @@ From Coq Require Import Min.
 From stdpp Require Import coPset.
 From iris.algebra Require Import big_op gmap frac agree.
 From iris.algebra Require Import csum excl auth cmra_big_op.
-From iris.base_logic Require Import big_op lib.fractional.
+From iris.bi Require Import fractional.
 From iris.base_logic Require Export lib.own.
 From iris.proofmode Require Export tactics.
 From lrust.lang Require Export lang.
@@ -71,21 +71,21 @@ Instance: Params (@heap_mapsto) 4.
 Instance: Params (@heap_freeable) 5.
 
 Notation "l ↦{ q } v" := (heap_mapsto l q v)
-  (at level 20, q at level 50, format "l  ↦{ q }  v") : uPred_scope.
-Notation "l ↦ v" := (heap_mapsto l 1 v) (at level 20) : uPred_scope.
+  (at level 20, q at level 50, format "l  ↦{ q }  v") : bi_scope.
+Notation "l ↦ v" := (heap_mapsto l 1 v) (at level 20) : bi_scope.
 
 Notation "l ↦∗{ q } vl" := (heap_mapsto_vec l q vl)
-  (at level 20, q at level 50, format "l  ↦∗{ q }  vl") : uPred_scope.
-Notation "l ↦∗ vl" := (heap_mapsto_vec l 1 vl) (at level 20) : uPred_scope.
+  (at level 20, q at level 50, format "l  ↦∗{ q }  vl") : bi_scope.
+Notation "l ↦∗ vl" := (heap_mapsto_vec l 1 vl) (at level 20) : bi_scope.
 
 Notation "l ↦∗{ q }: P" := (∃ vl, l ↦∗{ q } vl ∗ P vl)%I
-  (at level 20, q at level 50, format "l  ↦∗{ q }:  P") : uPred_scope.
+  (at level 20, q at level 50, format "l  ↦∗{ q }:  P") : bi_scope.
 Notation "l ↦∗: P " := (∃ vl, l ↦∗ vl ∗ P vl)%I
-  (at level 20, format "l  ↦∗:  P") : uPred_scope.
+  (at level 20, format "l  ↦∗:  P") : bi_scope.
 
 Notation "†{ q } l … n" := (heap_freeable l q n)
-  (at level 20, q at level 50, format "†{ q } l … n") : uPred_scope.
-Notation "† l … n" := (heap_freeable l 1 n) (at level 20) : uPred_scope.
+  (at level 20, q at level 50, format "†{ q } l … n") : bi_scope.
+Notation "† l … n" := (heap_freeable l 1 n) (at level 20) : bi_scope.
 
 Section to_heap.
   Implicit Types σ : state.
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index 88394b666c9cf6aa5322b6e4ab3077a1825d3ccf..86858ce87d21b26b9587c7011663d989af360348 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -2,7 +2,7 @@ From Coq.QArith Require Import Qcanon.
 From iris.base_logic.lib Require Import invariants.
 From iris.program_logic Require Import weakestpre.
 From iris.proofmode Require Import tactics.
-From iris.base_logic Require Import fractional.
+From iris.bi Require Import fractional.
 From iris.algebra Require Import excl csum frac auth.
 From lrust.lang Require Import lang proofmode notation new_delete.
 Set Default Proof Using "Type".
diff --git a/theories/lang/proofmode.v b/theories/lang/proofmode.v
index 9c7eb8132f905a61f97aa3350169011b0cd54d96..5371e45f9945d9ae8349468bc5b7100d80c552e1 100644
--- a/theories/lang/proofmode.v
+++ b/theories/lang/proofmode.v
@@ -9,7 +9,7 @@ Import uPred.
 Lemma tac_wp_value `{lrustG Σ} Δ E Φ e v :
   IntoVal e v →
   envs_entails Δ (Φ v) → envs_entails Δ (WP e @ E {{ Φ }}).
-Proof. rewrite /envs_entails=> ? ->. by apply wp_value. Qed.
+Proof. rewrite envs_entails_eq=> ? ->. by apply wp_value. Qed.
 
 Ltac wp_value_head := eapply tac_wp_value; [apply _|lazy beta].
 
@@ -20,7 +20,7 @@ Lemma tac_wp_pure `{lrustG Σ} K Δ Δ' E e1 e2 φ Φ :
   envs_entails Δ' (WP fill K e2 @ E {{ Φ }}) →
   envs_entails Δ (WP fill K e1 @ E {{ Φ }}).
 Proof.
-  rewrite /envs_entails=> ??? HΔ'. rewrite into_laterN_env_sound /=.
+  rewrite envs_entails_eq=> ??? HΔ'. rewrite into_laterN_env_sound /=.
   rewrite -wp_bind HΔ' -wp_pure_step_later //. by rewrite -wp_bind_inv.
 Qed.
 
@@ -45,8 +45,8 @@ Lemma tac_wp_eq_loc `{lrustG Σ} K Δ Δ' E i1 i2 l1 l2 q1 q2 v1 v2 Φ :
   envs_entails Δ' (WP fill K (Lit (bool_decide (l1 = l2))) @ E {{ Φ }}) →
   envs_entails Δ (WP fill K (BinOp EqOp (Lit (LitLoc l1)) (Lit (LitLoc l2))) @ E {{ Φ }}).
 Proof.
-  rewrite /envs_entails=> ? /envs_lookup_sound'. rewrite sep_elim_l=> ?.
-  move /envs_lookup_sound'; rewrite sep_elim_l=> ? HΔ. rewrite -wp_bind.
+  rewrite envs_entails_eq=> ? /envs_lookup_sound /=. rewrite sep_elim_l=> ?.
+  move /envs_lookup_sound; rewrite sep_elim_l=> ? HΔ. rewrite -wp_bind.
   rewrite into_laterN_env_sound /=. eapply wp_eq_loc; eauto using later_mono.
 Qed.
 
@@ -70,7 +70,7 @@ Tactic Notation "wp_case" := wp_pure (Case _ _); try wp_value_head.
 Lemma tac_wp_bind `{lrustG Σ} K Δ E Φ e :
   envs_entails Δ (WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }})%I →
   envs_entails Δ (WP fill K e @ E {{ Φ }}).
-Proof. rewrite /envs_entails=> ->. apply: wp_bind. Qed.
+Proof. rewrite envs_entails_eq=> ->. apply: wp_bind. Qed.
 
 Ltac wp_bind_core K :=
   lazymatch eval hnf in K with
@@ -92,7 +92,7 @@ Section heap.
 Context `{lrustG Σ}.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
-Implicit Types Δ : envs (iResUR Σ).
+Implicit Types Δ : envs (uPredI (iResUR Σ)).
 
 Lemma tac_wp_alloc K Δ Δ' E j1 j2 n Φ :
   0 < n →
@@ -103,12 +103,12 @@ Lemma tac_wp_alloc K Δ Δ' E j1 j2 n Φ :
     envs_entails Δ'' (WP fill K (Lit $ LitLoc l) @ E {{ Φ }})) →
   envs_entails Δ (WP fill K (Alloc (Lit $ LitInt n)) @ E {{ Φ }}).
 Proof.
-  rewrite /envs_entails=> ?? HΔ. rewrite -wp_bind.
+  rewrite envs_entails_eq=> ?? HΔ. rewrite -wp_bind.
   eapply wand_apply; first exact:wp_alloc.
-  rewrite -and_sep_l. apply and_intro; first auto with I.
+  rewrite -persistent_and_sep. apply and_intro; first auto with I.
   rewrite into_laterN_env_sound; apply later_mono, forall_intro=> l.
   apply forall_intro=>sz. apply wand_intro_l. rewrite -assoc.
-  apply pure_elim_sep_l=> Hn. apply wand_elim_r'.
+  rewrite sep_and. apply pure_elim_l=> Hn. apply wand_elim_r'.
   destruct (HΔ l sz) as (Δ''&?&HΔ'); first done.
   rewrite envs_app_sound //; simpl. by rewrite right_id HΔ'.
 Qed.
@@ -117,17 +117,17 @@ Lemma tac_wp_free K Δ Δ' Δ'' Δ''' E i1 i2 vl (n : Z) (n' : nat) l Φ :
   n = length vl →
   MaybeIntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i1 Δ' = Some (false, l ↦∗ vl)%I →
-  envs_delete i1 false Δ' = Δ'' →
+  envs_delete false i1 false Δ' = Δ'' →
   envs_lookup i2 Δ'' = Some (false, †l…n')%I →
-  envs_delete i2 false Δ'' = Δ''' →
+  envs_delete false i2 false Δ'' = Δ''' →
   n' = length vl →
   envs_entails Δ''' (WP fill K (Lit LitPoison) @ E {{ Φ }}) →
   envs_entails Δ (WP fill K (Free (Lit $ LitInt n) (Lit $ LitLoc l)) @ E {{ Φ }}).
 Proof.
-  rewrite /envs_entails; intros -> ?? <- ? <- -> HΔ. rewrite -wp_bind.
+  rewrite envs_entails_eq; intros -> ?? <- ? <- -> HΔ. rewrite -wp_bind.
   eapply wand_apply; first exact:wp_free; simpl.
   rewrite into_laterN_env_sound -!later_sep; apply later_mono.
-  do 2 (rewrite envs_lookup_sound' //). by rewrite HΔ wand_True -assoc.
+  do 2 (rewrite envs_lookup_sound //). by rewrite HΔ True_emp emp_wand -assoc.
 Qed.
 
 Lemma tac_wp_read K Δ Δ' E i l q v o Φ :
@@ -137,7 +137,7 @@ Lemma tac_wp_read K Δ Δ' E i l q v o Φ :
   envs_entails Δ' (WP fill K (of_val v) @ E {{ Φ }}) →
   envs_entails Δ (WP fill K (Read o (Lit $ LitLoc l)) @ E {{ Φ }}).
 Proof.
-  rewrite /envs_entails; intros [->| ->] ???.
+  rewrite envs_entails_eq; intros [->| ->] ???.
   - rewrite -wp_bind. eapply wand_apply; first exact:wp_read_na.
     rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
     by apply later_mono, sep_mono_r, wand_mono.
@@ -155,7 +155,7 @@ Lemma tac_wp_write K Δ Δ' Δ'' E i l v e v' o Φ :
   envs_entails Δ'' (WP fill K (Lit LitPoison) @ E {{ Φ }}) →
   envs_entails Δ (WP fill K (Write o (Lit $ LitLoc l) e) @ E {{ Φ }}).
 Proof.
-  rewrite /envs_entails; intros ? [->| ->] ????.
+  rewrite envs_entails_eq; intros ? [->| ->] ????.
   - rewrite -wp_bind. eapply wand_apply; first by apply wp_write_na.
     rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
     rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
diff --git a/theories/lifetime/at_borrow.v b/theories/lifetime/at_borrow.v
index 472f29ffa7930d0a17f609679f5a5134affbe873..3373c818dd6ccfd67e3209f9ba9c4060380bbfe2 100644
--- a/theories/lifetime/at_borrow.v
+++ b/theories/lifetime/at_borrow.v
@@ -9,7 +9,7 @@ Definition at_bor `{invG Σ, lftG Σ} κ N (P : iProp Σ) :=
   (∃ i, &{κ,i}P ∗
     (⌜N ## lftN⌝ ∗ inv N (idx_bor_own 1 i) ∨
      ⌜N = lftN⌝ ∗ inv N (∃ q, idx_bor_own q i)))%I.
-Notation "&at{ κ , N }" := (at_bor κ N) (format "&at{ κ , N }") : uPred_scope.
+Notation "&at{ κ , N }" := (at_bor κ N) (format "&at{ κ , N }") : bi_scope.
 
 Section atomic_bors.
   Context `{invG Σ, lftG Σ} (P : iProp Σ) (N : namespace).
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index f7c31e84c93edfaf9b820963589580e1821944c3..489ed417f683c52a75f19842e462d5b25af28e3f 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -1,6 +1,6 @@
 From Coq Require Import Qcanon.
 From iris.proofmode Require Import tactics.
-From iris.base_logic Require Import lib.fractional.
+From iris.bi Require Import fractional.
 From iris.algebra Require Import frac.
 From lrust.lifetime Require Export at_borrow.
 Set Default Proof Using "Type".
@@ -10,7 +10,7 @@ Class frac_borG Σ := frac_borG_inG :> inG Σ fracR.
 Definition frac_bor `{invG Σ, lftG Σ, frac_borG Σ} κ (φ : Qp → iProp Σ) :=
   (∃ γ κ', κ ⊑ κ' ∗ &at{κ',lftN} (∃ q, φ q ∗ own γ q ∗
                        (⌜q = 1%Qp⌝ ∨ ∃ q', ⌜(q + q' = 1)%Qp⌝ ∗ q'.[κ'])))%I.
-Notation "&frac{ κ }" := (frac_bor κ) (format "&frac{ κ }") : uPred_scope.
+Notation "&frac{ κ }" := (frac_bor κ) (format "&frac{ κ }") : bi_scope.
 
 Section frac_bor.
   Context `{invG Σ, lftG Σ, frac_borG Σ} (φ : Qp → iProp Σ).
@@ -78,7 +78,7 @@ Section frac_bor.
     iDestruct "H" as (qφ) "(Hφqφ & >Hown & Hq)".
     destruct (Qp_lower_bound (qκ'/2) (qφ/2)) as (qq & qκ'0 & qφ0 & Hqκ' & Hqφ).
     iExists qq.
-    iAssert (▷ φ qq ∗ ▷ φ (qφ0 + qφ / 2))%Qp%I with "[Hφqφ]" as "[$ Hqφ]".
+    iAssert (▷ (φ qq ∗ φ (qφ0 + qφ / 2)))%Qp%I with "[Hφqφ]" as "[$ Hqφ]".
     { iNext. rewrite -{1}(Qp_div_2 qφ) {1}Hqφ. iApply "Hφ". by rewrite assoc. }
     rewrite -{1}(Qp_div_2 qφ) {1}Hqφ -assoc {1}Hqκ'.
     iDestruct "Hκ2" as "[Hκq Hκqκ0]". iDestruct "Hown" as "[Hownq Hown]".
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index 22ba767772478e60dd18a8ad72d858924d63bd73..735ae6d1c528afce6c9c17addc0c685d4e686058 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -88,7 +88,7 @@ Lemma bor_or E κ P Q :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ}(P ∨ Q) ={E}=∗ (&{κ}P ∨ &{κ}Q).
 Proof.
-  iIntros (?) "#LFT H". rewrite uPred.or_alt.
+  iIntros (?) "#LFT H". rewrite bi.or_alt.
   (* The (A:=...) is needed due to Coq bug #5458 *)
   iMod (bor_exists (A:=bool) with "LFT H") as ([]) "H"; auto.
 Qed.
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 488f8293680505a242d201e693dbf40dd2741b4a..d0b5af77ba38a58979c1aea31c8f2025b29989cf 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -1,7 +1,8 @@
 From iris.algebra Require Import frac.
 From stdpp Require Export gmultiset strings.
 From iris.base_logic.lib Require Export invariants.
-From iris.base_logic.lib Require Import boxes fractional.
+From iris.base_logic.lib Require Import boxes.
+From iris.bi Require Import fractional.
 Set Default Proof Using "Type".
 
 Definition lftN : namespace := nroot .@ "lft".
@@ -36,13 +37,13 @@ Module Type lifetime_sig.
 
   (** Notation *)
   Notation "q .[ κ ]" := (lft_tok q κ)
-      (format "q .[ κ ]", at level 0) : uPred_scope.
-  Notation "[† κ ]" := (lft_dead κ) (format "[† κ ]"): uPred_scope.
+      (format "q .[ κ ]", at level 0) : bi_scope.
+  Notation "[† κ ]" := (lft_dead κ) (format "[† κ ]"): bi_scope.
 
-  Notation "&{ κ }" := (bor κ) (format "&{ κ }") : uPred_scope.
-  Notation "&{ κ , i }" := (idx_bor κ i) (format "&{ κ , i }") : uPred_scope.
+  Notation "&{ κ }" := (bor κ) (format "&{ κ }") : bi_scope.
+  Notation "&{ κ , i }" := (idx_bor κ i) (format "&{ κ , i }") : bi_scope.
 
-  Infix "⊑" := lft_incl (at level 70) : uPred_scope.
+  Infix "⊑" := lft_incl (at level 70) : bi_scope.
   Infix "⊓" := lft_intersect (at level 40) : stdpp_scope.
 
   Section properties.
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 1dbe120693d240af40513016a8e528b6c35122a1..14f35f7f7447c87309f24fff5b143b0d967bed43 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -1,7 +1,6 @@
 From lrust.lifetime Require Export primitive.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import csum auth frac gmap agree gset.
-From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
 Set Default Proof Using "Type".
 
@@ -202,7 +201,7 @@ Proof.
         iLeft. iFrame "%". iExists _, _. iFrame. }
       iMod ("Hclose" with "Htok") as "$". iExists κ''. iModIntro.
       iSplit; first by iApply lft_incl_refl. iExists j. iFrame.
-      iExists Q. rewrite -uPred.iff_refl. eauto.
+      iExists Q. rewrite -bi.iff_refl. eauto.
     + iDestruct "Hinv" as (?) "[Hinv _]". iDestruct "Hinv" as (B ?) "[>Hinv _]".
       iDestruct (own_bor_valid_2 with "Hinv Hbor")
         as %[(_ & <- & INCL%option_included)%singleton_included _]%auth_valid_discrete_2.
@@ -249,7 +248,7 @@ Proof.
     rewrite own_bor_op. iDestruct "Hown" as "[H● H◯]".
     iMod ("Hclose'" with "[- Hâ—¯]"); last first.
     { iModIntro. iExists (i.1). iSplit; first by iApply lft_incl_refl.
-      iExists j. iFrame. iExists Q. rewrite -uPred.iff_refl. auto. }
+      iExists j. iFrame. iExists Q. rewrite -bi.iff_refl. auto. }
     iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
     iLeft. iFrame "%". iExists _, _. iFrame. iNext.
     rewrite -!fmap_delete -fmap_insert -(fmap_insert _ _ _ Bor_in).
diff --git a/theories/lifetime/model/borrow.v b/theories/lifetime/model/borrow.v
index 5d3f286498c222b9e16d57297f1b6254a7166d26..8138b837bb99d948c8d83c1393c749c513f89e19 100644
--- a/theories/lifetime/model/borrow.v
+++ b/theories/lifetime/model/borrow.v
@@ -1,7 +1,6 @@
 From lrust.lifetime Require Export primitive.
 From lrust.lifetime Require Export faking.
 From iris.algebra Require Import csum auth frac gmap agree gset.
-From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
@@ -44,7 +43,7 @@ Proof.
     iMod ("Hclose" with "[HA HI Hclose']") as "_"; [by iNext; iExists _, _; iFrame|].
     iSplitL "HBâ—¯ HsliceB".
     + rewrite /bor /raw_bor /idx_bor_own. iModIntro. iExists γB. iFrame.
-      iExists P. rewrite -uPred.iff_refl. auto.
+      iExists P. rewrite -bi.iff_refl. auto.
     + clear -HE. iIntros "!> H†".
       iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
       iDestruct ("HIlookup" with "HI") as %Hκ.
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index 4c8c24fbb216e07f418bc658b16fe8d243e01df3..60be506be7cdafd528e641c0d6971e99ec913271 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -1,7 +1,6 @@
 From lrust.lifetime Require Export primitive.
 From lrust.lifetime Require Export faking reborrow.
 From iris.algebra Require Import csum auth frac gmap agree.
-From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
@@ -52,10 +51,10 @@ Proof.
     rewrite !own_bor_op. iDestruct "Hbor" as "[[H● H◯2] H◯1]".
     iAssert (&{κ}P)%I with "[H◯1 Hs1]" as "$".
     { rewrite /bor /raw_bor /idx_bor_own. iExists κ'. iFrame "#". iExists γ1.
-      iFrame. iExists P. rewrite -uPred.iff_refl. auto. }
+      iFrame. iExists P. rewrite -bi.iff_refl. auto. }
     iAssert (&{κ}Q)%I with "[H◯2 Hs2]" as "$".
     { rewrite /bor /raw_bor /idx_bor_own. iExists κ'. iFrame "#". iExists γ2.
-      iFrame. iExists Q. rewrite -uPred.iff_refl. auto. }
+      iFrame. iExists Q. rewrite -bi.iff_refl. auto. }
     iApply "Hclose". iExists A, I. iFrame. rewrite big_sepS_later.
     iApply "Hclose'". iLeft. iFrame "%". iExists Pb', Pi. iFrame. iExists _.
     rewrite /to_borUR -!fmap_delete -!fmap_insert. iFrame "Hbox H●".
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 1861dd1b7527a4a41e09cfe8926f56e835ea2b34..00d6a80e669aa5771f258aaa6a9469ee65376549 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -1,7 +1,6 @@
 From lrust.lifetime Require Export primitive.
 From lrust.lifetime Require Import faking.
 From iris.algebra Require Import csum auth frac gmap agree gset.
-From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 22988966a663cc6ce7dd7740c6bfa236539e0b9d..c44b0486477cc8a27c09a013927d3a5d193bb544 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -1,5 +1,4 @@
 From iris.algebra Require Import csum auth frac gmap agree gset.
-From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
 From lrust.lifetime Require Export lifetime_sig.
 Set Default Proof Using "Type".
@@ -209,13 +208,13 @@ Instance raw_bor_params : Params (@raw_bor) 4.
 Instance bor_params : Params (@bor) 4.
 
 Notation "q .[ κ ]" := (lft_tok q κ)
-    (format "q .[ κ ]", at level 0) : uPred_scope.
-Notation "[† κ ]" := (lft_dead κ) (format "[† κ ]"): uPred_scope.
+    (format "q .[ κ ]", at level 0) : bi_scope.
+Notation "[† κ ]" := (lft_dead κ) (format "[† κ ]"): bi_scope.
 
-Notation "&{ κ }" := (bor κ) (format "&{ κ }") : uPred_scope.
-Notation "&{ κ , i }" := (idx_bor κ i) (format "&{ κ , i }") : uPred_scope.
+Notation "&{ κ }" := (bor κ) (format "&{ κ }") : bi_scope.
+Notation "&{ κ , i }" := (idx_bor κ i) (format "&{ κ , i }") : bi_scope.
 
-Infix "⊑" := lft_incl (at level 70) : uPred_scope.
+Infix "⊑" := lft_incl (at level 70) : bi_scope.
 
 (* TODO: Making all these things opaque is rather annoying, we should
    find a way to avoid it, or *at least*, to avoid having to manually unfold
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index dfb8359c6aaa9c19a39ef298fe59f4caf736877a..c00558ab0e1038044fe94f4f28bd590f6c0da31b 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -1,6 +1,5 @@
 From lrust.lifetime Require Export primitive.
 From iris.algebra Require Import csum auth frac gmap agree gset.
-From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
@@ -89,7 +88,7 @@ Proof.
     by do 2 eapply lookup_to_gmap_None. }
   rewrite /bor /raw_bor /idx_bor_own /=. iModIntro. iSplitR "Hâ—¯".
   - iExists ({[γ]} ∪ B), (P ∗ Pinh)%I. rewrite !to_gmap_union_singleton. by iFrame.
-  - iExists γ. iFrame. iExists P. rewrite -uPred.iff_refl. eauto.
+  - iExists γ. iFrame. iExists P. rewrite -bi.iff_refl. eauto.
 Qed.
 
 Lemma raw_bor_fake' E κ P :
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 629093d78de5622c30b49f2f2e5a4f4f2dbf5624..038aa8d1b47a93182ef95be688f661ec1e463381 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -1,7 +1,7 @@
 From lrust.lifetime.model Require Export definitions.
-From iris.algebra Require Import csum auth frac gmap agree gset.
-From iris.base_logic Require Import big_op.
-From iris.base_logic.lib Require Import boxes fractional.
+From iris.algebra Require Import csum auth frac gmap agree gset proofmode_classes.
+From iris.base_logic.lib Require Import boxes.
+From iris.bi Require Import fractional.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 Import uPred.
@@ -70,9 +70,9 @@ Proof.
   iExists γs. iSplit. done. rewrite own_op; iFrame.
 Qed.
 Global Instance own_bor_into_op κ x x1 x2 :
-  IsOp x x1 x2 → IntoAnd false (own_bor κ x) (own_bor κ x1) (own_bor κ x2).
+  IsOp x x1 x2 → IntoSep (own_bor κ x) (own_bor κ x1) (own_bor κ x2).
 Proof.
-  rewrite /IsOp /IntoAnd=>->. by rewrite -own_bor_op.
+  rewrite /IsOp /IntoSep=>-> /=. by rewrite -own_bor_op.
 Qed.
 Lemma own_bor_valid κ x : own_bor κ x -∗ ✓ x.
 Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
@@ -104,9 +104,9 @@ Proof.
   iExists γs. iSplit; first done. rewrite own_op; iFrame.
 Qed.
 Global Instance own_cnt_into_op κ x x1 x2 :
-  IsOp x x1 x2 → IntoAnd false (own_cnt κ x) (own_cnt κ x1) (own_cnt κ x2).
+  IsOp x x1 x2 → IntoSep (own_cnt κ x) (own_cnt κ x1) (own_cnt κ x2).
 Proof.
-  rewrite /IsOp /IntoAnd=> /leibniz_equiv_iff->. by rewrite -own_cnt_op.
+  rewrite /IsOp /IntoSep=> /leibniz_equiv_iff->. by rewrite -own_cnt_op.
 Qed.
 Lemma own_cnt_valid κ x : own_cnt κ x -∗ ✓ x.
 Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
@@ -138,9 +138,9 @@ Proof.
   iExists γs. iSplit. done. rewrite own_op; iFrame.
 Qed.
 Global Instance own_inh_into_op κ x x1 x2 :
-  IsOp x x1 x2 → IntoAnd false (own_inh κ x) (own_inh κ x1) (own_inh κ x2).
+  IsOp x x1 x2 → IntoSep (own_inh κ x) (own_inh κ x1) (own_inh κ x2).
 Proof.
-  rewrite /IsOp /IntoAnd=> /leibniz_equiv_iff->. by rewrite -own_inh_op.
+  rewrite /IsOp /IntoSep=> /leibniz_equiv_iff->. by rewrite -own_inh_op.
 Qed.
 Lemma own_inh_valid κ x : own_inh κ x -∗ ✓ x.
 Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
@@ -275,7 +275,7 @@ Qed.
 Lemma lft_tok_dead q κ : q.[κ] -∗ [† κ] -∗ False.
 Proof.
   rewrite /lft_tok /lft_dead. iIntros "H"; iDestruct 1 as (Λ') "[% H']".
-  iDestruct (big_sepMS_elem_of _ _ Λ' with "H") as "H"=> //.
+  iDestruct (@big_sepMS_elem_of _ _ _ _ _ _ Λ' with "H") as "H"=> //.
   iDestruct (own_valid_2 with "H H'") as %Hvalid.
   move: Hvalid=> /auth_own_valid /=; by rewrite op_singleton singleton_valid.
 Qed.
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index f73146de35580395f509484fb5a066ab2a5aa2d0..5187975f12e34ae0fc8c8d66fbaebb2d25c99b93 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -1,6 +1,5 @@
 From lrust.lifetime Require Import borrow accessors.
 From iris.algebra Require Import csum auth frac gmap agree gset.
-From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
@@ -61,7 +60,7 @@ Proof.
      (alloc_singleton_local_update _ j (1%Qp, to_agree Bor_in)); last done.
     rewrite /to_borUR lookup_fmap. by rewrite HBj. }
   iModIntro. iExists (P ∗ Pb)%I. rewrite /Iinv. iFrame "HI Hκ". iSplitL "Hj".
-  { iExists j. iFrame. iExists P. rewrite -uPred.iff_refl. auto. }
+  { iExists j. iFrame. iExists P. rewrite -bi.iff_refl. auto. }
   iSplitL "Hbox HB● HB".
   { rewrite /lft_bor_alive. iNext. iExists (<[j:=Bor_in]> B).
     rewrite /to_borUR !fmap_insert big_sepM_insert //. iFrame.
diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index bac68ad60daaffc26752a8434468f73431b027e7..415516877fa114e66db68a468321a91b5eb9bc16 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -8,7 +8,7 @@ Definition na_bor `{invG Σ, lftG Σ, na_invG Σ}
   (∃ i, &{κ,i}P ∗ na_inv tid N (idx_bor_own 1 i))%I.
 
 Notation "&na{ κ , tid , N }" := (na_bor κ tid N)
-    (format "&na{ κ , tid , N }") : uPred_scope.
+    (format "&na{ κ , tid , N }") : bi_scope.
 
 Section na_bor.
   Context `{invG Σ, lftG Σ, na_invG Σ}
diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index 08784b1a57c986e030cbc44b531c438b0945a2be..4a4d6a15b0336f088fb9a0e3b427528b7b835378 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -1,4 +1,3 @@
-From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
 From lrust.typing Require Export type.
 From lrust.typing Require Import programs.
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 680dca3836712263ba6a0edc110c0d4f3f2523cb..6ab6044295b8b3630bc340114b51fec622c9eb5a 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -1,5 +1,4 @@
 From iris.proofmode Require Import tactics.
-From iris.base_logic Require Import big_op.
 From lrust.lang Require Import proofmode.
 From lrust.typing Require Export uniq_bor shr_bor own.
 From lrust.typing Require Import lft_contexts type_context programs.
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index c25ab6b1b3ac3c6b99642ee1c091f6287de888d9..02ef7650e5508e4fca52969098380e70c59eee2f 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -1,4 +1,3 @@
-From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
 From lrust.typing Require Export type.
 From lrust.typing Require Import programs.
diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index 0dac90dfd986066976959172bbecfc21de219cc0..a86297a4794aea8a71e6c4dd27cc6f12dc44fd12 100644
--- a/theories/typing/cont_context.v
+++ b/theories/typing/cont_context.v
@@ -1,5 +1,4 @@
 From iris.proofmode Require Import tactics.
-From iris.base_logic Require Import big_op.
 From lrust.lang Require Import notation.
 From lrust.typing Require Import type lft_contexts type_context.
 Set Default Proof Using "Type".
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index fb89f3fae4059dc0e20b7a2646e7db22fe4cd40f..f93012b0002611a21f60bb66813273680f035b24 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -60,8 +60,8 @@ Section fixpoint.
       eapply (limit_preserving_ext (λ _, _ ∧ _)).
       { split; (intros [H1 H2]; split; [apply H1|apply H2]). }
       apply limit_preserving_and; repeat (apply limit_preserving_forall=> ?).
-      + apply uPred.limit_preserving_Persistent; solve_proper.
-      + apply limit_preserving_impl, uPred.limit_preserving_entails;
+      + apply bi.limit_preserving_Persistent; solve_proper.
+      + apply limit_preserving_impl, bi.limit_preserving_entails;
         solve_proper_core ltac:(fun _ => eapply ty_size_ne || f_equiv).
   Qed.
 
@@ -74,7 +74,7 @@ Section fixpoint.
     - exists bool. apply _.
     - done.
     - repeat (apply limit_preserving_forall=> ?).
-      apply uPred.limit_preserving_entails; solve_proper.
+      apply bi.limit_preserving_entails; solve_proper.
   Qed.
 
   Global Instance fixpoint_sync :
@@ -86,7 +86,7 @@ Section fixpoint.
     - exists bool. apply _.
     - done.
     - repeat (apply limit_preserving_forall=> ?).
-      apply uPred.limit_preserving_entails; solve_proper.
+      apply bi.limit_preserving_entails; solve_proper.
   Qed.
 
   Lemma fixpoint_unfold_eqtype E L : eqtype E L (type_fixpoint T) (T (type_fixpoint T)).
@@ -111,7 +111,7 @@ Section subtyping.
     - by eexists _.
     - intros. setoid_rewrite (fixpoint_unfold_eqtype T2). by apply H12.
     - repeat (apply limit_preserving_forall=> ?).
-      apply uPred.limit_preserving_entails; solve_proper.
+      apply bi.limit_preserving_entails; solve_proper.
   Qed.
 
   Lemma fixpoint_proper T1 `{TypeContractive T1} T2 `{TypeContractive T2} :
@@ -124,7 +124,7 @@ Section subtyping.
     - by eexists _.
     - intros. setoid_rewrite (fixpoint_unfold_eqtype T2). by apply H12.
     - apply limit_preserving_and; repeat (apply limit_preserving_forall=> ?);
-        apply uPred.limit_preserving_entails; solve_proper.
+        apply bi.limit_preserving_entails; solve_proper.
   Qed.
 
   Lemma fixpoint_unfold_subtype_l ty T `{TypeContractive T} :
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 69362f451aa2656be5e68bb92804e100a7909f38..06b711f56f2ae27a1e62f9bf53645d869be6b1c9 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -1,6 +1,5 @@
-From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import vector.
+From iris.algebra Require Import vector list.
 From lrust.typing Require Export type.
 From lrust.typing Require Import own programs cont.
 Set Default Proof Using "Type".
@@ -88,23 +87,17 @@ Section fn.
       do 5 f_equiv. apply type_dist2_dist. apply Hfp.
     - rewrite /tctx_interp !big_sepL_zip_with /=. do 4 f_equiv.
       cut (∀ n tid p i, Proper (dist n ==> dist n)
-        (λ (l : list _), ∀ ty, ⌜l !! i = Some ty⌝ → tctx_elt_interp tid (p ◁ ty))%I).
+        (λ (l : list type),
+            match l !! i with
+            | Some ty => tctx_elt_interp tid (p ◁ ty) | None => emp
+            end)%I).
       { intros Hprop. apply Hprop, list_fmap_ne; last first.
         - symmetry. eapply Forall2_impl; first apply Hfp. intros.
           apply dist_later_dist, type_dist2_dist_later. done.
         - apply _. }
-      clear. intros n tid p i x y. rewrite list_dist_lookup=>Hxy.
-      specialize (Hxy i). destruct (x !! i) as [tyx|], (y !! i) as [tyy|];
-        inversion_clear Hxy; last done.
-      transitivity (tctx_elt_interp tid (p ◁ tyx));
-        last transitivity (tctx_elt_interp tid (p ◁ tyy)); last 2 first.
-      + unfold tctx_elt_interp. do 3 f_equiv. by apply ty_own_ne.
-      + apply equiv_dist. iSplit.
-        * iIntros "H * #EQ". by iDestruct "EQ" as %[=->].
-        * iIntros "H". by iApply "H".
-      + apply equiv_dist. iSplit.
-        * iIntros "H". by iApply "H".
-        * iIntros "H * #EQ". by iDestruct "EQ" as %[=->].
+      clear. intros n tid p i x y. rewrite list_dist_lookup=>/(_ i).
+      case _ : (x !! i)=>[tyx|]; case  _ : (y !! i)=>[tyy|];
+        inversion_clear 1; [solve_proper|done].
   Qed.
 
   Global Instance fn_ne n' :
@@ -191,15 +184,15 @@ Section typing.
          -{2}(fst_zip (fp x).(fp_tys) (fp' x).(fp_tys)) ?vec_to_list_length //
          -{2}(snd_zip (fp x).(fp_tys) (fp' x).(fp_tys)) ?vec_to_list_length //
          !zip_with_fmap_r !(zip_with_zip (λ _ _, (_ ∘ _) _ _)) !big_sepL_fmap.
-      iApply big_sepL_impl. iSplit; last done. iIntros "{HT Hty}!#".
+      iApply (big_sepL_impl with "HT"). iIntros "!#".
       iIntros (i [p [ty1' ty2']]) "#Hzip H /=".
       iDestruct "H" as (v) "[? Hown]". iExists v. iFrame.
       rewrite !lookup_zip_with.
       iDestruct "Hzip" as %(? & ? & ([? ?] & (? & Hty'1 &
         (? & Hty'2 & [=->->])%bind_Some)%bind_Some & [=->->->])%bind_Some)%bind_Some.
-      iDestruct (big_sepL_lookup with "Htys") as "#Hty".
+      iDestruct (big_sepL_lookup with "Htys") as "#Hty'".
       { rewrite lookup_zip_with /=. erewrite Hty'2. simpl. by erewrite Hty'1. }
-      iDestruct (box_type_incl with "[$Hty]") as "(_ & #Hincl & _)".
+      iDestruct (box_type_incl with "[$Hty']") as "(_ & #Hincl & _)".
       by iApply "Hincl".
   Qed.
 
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index d1506438c7736ef4783b4e5840940fb7c52b3202..1291369424c080fc27f4fe79cd15820b747aa254 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -1,6 +1,5 @@
 From iris.proofmode Require Import tactics.
-From iris.base_logic Require Import big_op.
-From iris.base_logic.lib Require Import fractional.
+From iris.bi Require Import fractional.
 From lrust.lang Require Import proofmode.
 From lrust.typing Require Export base.
 From lrust.lifetime Require Import frac_borrow.
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index ce484f170cdb31e8186df836a47538906d9691c4..fcd2e3702921677073d2ef6900907d4d1ea83e25 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -1,7 +1,7 @@
 From Coq.QArith Require Import Qcanon.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree.
-From iris.base_logic Require Import big_op fractional.
+From iris.bi Require Import fractional.
 From lrust.lang.lib Require Import memcpy arc.
 From lrust.lifetime Require Import at_borrow.
 From lrust.typing Require Export type.
@@ -203,7 +203,7 @@ Section arc.
   Proof.
     intros Hse Hsy tid tid' vl. destruct vl as [|[[|l|]|] []]=>//=.
     unfold full_arc_own, shared_arc_own.
-    repeat (apply send_change_tid || apply uPred.exist_mono ||
+    repeat (apply send_change_tid || apply bi.exist_mono ||
             (apply arc_persist_send; apply _) || f_equiv || intros ?).
   Qed.
 
@@ -211,7 +211,7 @@ Section arc.
     Send ty → Sync ty → Sync (arc ty).
   Proof.
     intros Hse Hsy ν tid tid' l.
-    repeat (apply send_change_tid || apply uPred.exist_mono ||
+    repeat (apply send_change_tid || apply bi.exist_mono ||
             (apply arc_persist_send; apply _) || f_equiv || intros ?).
   Qed.
 
@@ -311,7 +311,7 @@ Section arc.
     Send ty → Sync ty → Send (weak ty).
   Proof.
     intros Hse Hsy tid tid' vl. destruct vl as [|[[|l|]|] []]=>//=.
-    repeat (apply send_change_tid || apply uPred.exist_mono ||
+    repeat (apply send_change_tid || apply bi.exist_mono ||
             (apply arc_persist_send; apply _) || f_equiv || intros ?).
   Qed.
 
@@ -319,7 +319,7 @@ Section arc.
     Send ty → Sync ty → Sync (weak ty).
   Proof.
     intros Hse Hsy ν tid tid' l.
-    repeat (apply send_change_tid || apply uPred.exist_mono ||
+    repeat (apply send_change_tid || apply bi.exist_mono ||
             (apply arc_persist_send; apply _) || f_equiv || intros ?).
   Qed.
 
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 4afcfed740c482ffaf0067f19adda89a1bc4b5e6..dea59d49a8641bf1d121dd0989bdc690eae76301 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -1,5 +1,4 @@
 From iris.proofmode Require Import tactics.
-From iris.base_logic Require Import big_op.
 From lrust.lang.lib Require Import memcpy.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Export type.
@@ -40,7 +39,7 @@ Section cell.
     iDestruct ("EQ" with "HE") as "(% & #Hown & #Hshr)".
     iSplit; [done|iSplit; iIntros "!# * H"].
     - iApply ("Hown" with "H").
-    - iApply na_bor_iff; last done. iSplit; iIntros "!>!# H";
+    - iApply na_bor_iff; last done. iNext; iAlways; iSplit; iIntros "H";
       iDestruct "H" as (vl) "[??]"; iExists vl; iFrame; by iApply "Hown".
   Qed.
   Lemma cell_mono' E L ty1 ty2 : eqtype E L ty1 ty2 → subtype E L (cell ty1) (cell ty2).
diff --git a/theories/typing/lib/diverging_static.v b/theories/typing/lib/diverging_static.v
index 6926982a824c874a50dce9a5a63148191f19d4c0..b07fdb62896f4c7cdb6ce9a28c33a5fe92d7e430 100644
--- a/theories/typing/lib/diverging_static.v
+++ b/theories/typing/lib/diverging_static.v
@@ -1,5 +1,4 @@
 From iris.proofmode Require Import tactics.
-From iris.base_logic Require Import big_op.
 From lrust.typing Require Export type.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
@@ -23,7 +22,7 @@ Section diverging_static.
     (* F : FnOnce(&'static T), as witnessed by the impl call_once *)
     typed_val call_once (fn(∅; F, &shr{static} T) → unit) →
     typed_val (diverging_static_loop call_once)
-              (fn(∀ α, λ ϝ, T.(ty_outlives_E) static; &shr{α} T, F) → emp).
+              (fn(∀ α, λ ϝ, T.(ty_outlives_E) static; &shr{α} T, F) → ∅).
   Proof.
     intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x f. simpl_subst.
diff --git a/theories/typing/lib/fake_shared_box.v b/theories/typing/lib/fake_shared_box.v
index 35c849e5b75840d0c9da4a59170bf619a942665e..d6cb31f45f43ea83c1d4d15927916303e714b082 100644
--- a/theories/typing/lib/fake_shared_box.v
+++ b/theories/typing/lib/fake_shared_box.v
@@ -1,5 +1,4 @@
 From iris.proofmode Require Import tactics.
-From iris.base_logic Require Import big_op.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/lib/join.v b/theories/typing/lib/join.v
index b11f27ef6adbf548dc6740dc0d60de71ee80c806..f1df0427576a2c3ae7254b18e29f2f4282c58752 100644
--- a/theories/typing/lib/join.v
+++ b/theories/typing/lib/join.v
@@ -1,5 +1,4 @@
 From iris.proofmode Require Import tactics.
-From iris.base_logic Require Import big_op.
 From lrust.lang Require Import spawn.
 From lrust.typing Require Export type.
 From lrust.typing Require Import typing.
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index 58e43755ed86cddb56ed305a54c871d9f9d66149..e1935d628cf1279b0bff941de89b189786902db1 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -1,7 +1,6 @@
 From Coq.QArith Require Import Qcanon.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree.
-From iris.base_logic Require Import big_op.
 From lrust.lang.lib Require Import memcpy lock.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Export type.
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index 507f88e0ed07f90c63f0c2cd02ecf99aad6105a4..be34421cd08f69ae4577661b3a0af512673d3800 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -1,7 +1,6 @@
 From Coq.QArith Require Import Qcanon.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree.
-From iris.base_logic Require Import big_op.
 From lrust.lang.lib Require Import memcpy lock.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Export type.
@@ -122,7 +121,7 @@ Section mguard.
   Global Instance mutexguard_sync α ty :
     Sync ty → Sync (mutexguard α ty).
   Proof.
-    move=>?????/=. apply uPred.exist_mono=>?. do 6 f_equiv.
+    move=>?????/=. apply bi.exist_mono=>?. do 7 f_equiv.
     by rewrite sync_change_tid.
   Qed.
 
diff --git a/theories/typing/lib/panic.v b/theories/typing/lib/panic.v
index a827be9c9e2eeb0dac3fb26a9958a7e5a95912e3..5296c6c4c7ac7d9d63548977860c605295f10dc2 100644
--- a/theories/typing/lib/panic.v
+++ b/theories/typing/lib/panic.v
@@ -16,7 +16,7 @@ Section panic.
   Definition panic : val :=
     funrec: <> [] := #☠.
 
-  Lemma panic_type : typed_val panic (fn(∅) → emp).
+  Lemma panic_type : typed_val panic (fn(∅) → ∅).
   Proof.
     intros E L. iApply type_fn; [done|]. iIntros "!# *".
     inv_vec args.  iIntros (tid) "LFT HE Hna HL Hk HT /=". simpl_subst.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 2ab6d344e6cc1a7a911f087800e27e738a5392c4..25061bdd0106d1835e93324c7ad88853b1fcd201 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -1,7 +1,6 @@
 From Coq.QArith Require Import Qcanon.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree.
-From iris.base_logic Require Import big_op.
 From lrust.lang.lib Require Import memcpy.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Export type.
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 291c57a7ef20ec02d4510ec8733fc75df6a3203c..311caf7eee99d5ab3acac6189f8f56a3b9d50b7d 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -1,7 +1,6 @@
 From Coq.QArith Require Import Qcanon.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree.
-From iris.base_logic Require Import big_op.
 From lrust.lang.lib Require Import memcpy.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Export type.
diff --git a/theories/typing/lib/refcell/ref.v b/theories/typing/lib/refcell/ref.v
index d5307a398869d2fb9f5844016c8ae6beba11bcac..5740462312e51f76b18ef205c6251d2809a29c83 100644
--- a/theories/typing/lib/refcell/ref.v
+++ b/theories/typing/lib/refcell/ref.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree.
-From iris.base_logic Require Import big_op fractional.
+From iris.bi Require Import fractional.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Import typing.
 From lrust.typing.lib.refcell Require Import refcell.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index b37cfeb51ae331b0e90b7e9b64b80899ee6b525e..f70befa86730c0da81b02237931496eba4e11f6e 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -1,7 +1,7 @@
 From Coq.QArith Require Import Qcanon.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree.
-From iris.base_logic Require Import big_op fractional.
+From iris.bi Require Import fractional.
 From lrust.lifetime Require Import lifetime na_borrow.
 From lrust.typing Require Import typing.
 From lrust.typing.lib.refcell Require Import refcell ref.
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index efdb9d10f8f207e93d9a98ca726d39306ad520e9..7223ac082cde921ce47680bca36ba4cc1572e1c9 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree.
-From iris.base_logic Require Import big_op fractional.
+From iris.bi Require Import fractional.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
@@ -75,7 +75,7 @@ Section refcell_inv.
     iAssert (□ (&{α}((l +ₗ 1) ↦∗: ty_own ty1 tid) -∗
                 &{α}((l +ₗ 1) ↦∗: ty_own ty2 tid)))%I as "#Hb".
     { iIntros "!# H". iApply bor_iff; last done.
-      iSplit; iIntros "!>!#H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl;
+      iNext; iAlways; iSplit; iIntros "H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl;
       iFrame; by iApply "Hown". }
     iDestruct "H" as (st) "H"; iExists st;
       iDestruct "H" as "($&$&H)"; destruct st as [[agν st]|]; try done;
@@ -184,7 +184,7 @@ Section refcell.
     - iPureIntro. simpl. congruence.
     - destruct vl as [|[[]|]]; try done. iDestruct "H" as "[$ H]". by iApply "Hown".
     - iDestruct "H" as (a γ) "[Ha H]". iExists a, γ. iFrame.
-      iApply na_bor_iff; last done. iSplit; iIntros "!>!# H".
+      iApply na_bor_iff; last done. iNext; iAlways; iSplit; iIntros "H".
       by iApply "Hty1ty2". by iApply "Hty2ty1".
   Qed.
   Lemma refcell_mono' E L ty1 ty2 :
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index b5c9942143058ddf57d8530e068f76a0fc570bd1..a571826adba7aa73a1cd9fa291c2c978f6a55893 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -1,7 +1,7 @@
 From Coq.QArith Require Import Qcanon.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree.
-From iris.base_logic Require Import big_op fractional.
+From iris.bi Require Import fractional.
 From lrust.lang.lib Require Import memcpy.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Import typing option.
diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v
index f9a2ec9129e334e65afd24858bd6ef1e4bbba181..790cdcec615dd815ba6caeb0c4c690b9bfb7ccb0 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree.
-From iris.base_logic Require Import big_op fractional.
+From iris.bi Require Import fractional.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Import typing util.
 From lrust.typing.lib.refcell Require Import refcell.
@@ -93,7 +93,7 @@ Section refmut.
       iExists ν, γ, β, ty'. iFrame "∗#". iSplit.
       + iApply bor_shorten; last iApply bor_iff; last done.
         * iApply lft_intersect_mono; first done. iApply lft_incl_refl.
-        * iSplit; iIntros "!>!# H"; iDestruct "H" as (vl) "[??]";
+        * iNext; iAlways; iSplit; iIntros "H"; iDestruct "H" as (vl) "[??]";
           iExists vl; iFrame; by iApply "Ho".
       + by iApply lft_incl_trans.
     - iIntros (κ tid l) "H". iDestruct "H" as (lv lrc) "H". iExists lv, lrc.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index e2f0360b26adab61d4b452f113ea1be336bc9d2f..443129c23d698977f2a4255d0d877f4414c8bb9f 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -1,7 +1,7 @@
 From Coq.QArith Require Import Qcanon.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree.
-From iris.base_logic Require Import big_op fractional.
+From iris.bi Require Import fractional.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Import typing.
 From lrust.typing.lib.refcell Require Import refcell refmut.
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 67d1092e49d822318192aec87deb5289424992ce..2ee4f34a7428d4fcc35da1b2684d69753ef44bfe 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree.
-From iris.base_logic Require Import big_op fractional.
+From iris.bi Require Import fractional.
 From lrust.lifetime Require Import at_borrow.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
@@ -71,7 +71,7 @@ Section rwlock_inv.
     iAssert (□ (&{α}((l +ₗ 1) ↦∗: ty_own ty1 tid) -∗
                 &{α}((l +ₗ 1) ↦∗: ty_own ty2 tid)))%I as "#Hb".
     { iIntros "!# H". iApply bor_iff; last done.
-      iSplit; iIntros "!>!#H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl;
+      iNext; iAlways; iSplit; iIntros "H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl;
       iFrame; by iApply "Hown". }
     iDestruct "H" as (st) "H"; iExists st;
       iDestruct "H" as "($&$&H)"; destruct st as [[|[[agν ?]?]|]|]; try done;
@@ -177,7 +177,7 @@ Section rwlock.
     - iPureIntro. simpl. congruence.
     - destruct vl as [|[[]|]]; try done. iDestruct "H" as "[$ H]". by iApply "Hown".
     - iDestruct "H" as (a γ) "[Ha H]". iExists a, γ. iFrame.
-      iApply at_bor_iff; last done. iSplit; iIntros "!>!# H".
+      iApply at_bor_iff; last done. iNext; iAlways; iSplit; iIntros "H".
       by iApply "Hty1ty2". by iApply "Hty2ty1".
   Qed.
   Lemma rwlock_mono' E L ty1 ty2 :
@@ -198,12 +198,12 @@ Section rwlock.
   Global Instance rwlock_sync :
     Send ty → Sync ty → Sync (rwlock ty).
   Proof.
-    move=>???????/=. do 2 apply uPred.exist_mono=>?. apply uPred.sep_mono_r.
-    iApply at_bor_iff. iIntros "!> !#". iApply uPred.equiv_iff.
-    apply uPred.exist_proper=>?; do 7 f_equiv; first do 7 f_equiv.
-    - do 5 f_equiv. apply uPred.equiv_spec; split; iApply send_change_tid.
-    - apply uPred.equiv_spec; split; iApply sync_change_tid.
-    - apply uPred.equiv_spec; split; iApply send_change_tid.
+    move=>???????/=. do 2 apply bi.exist_mono=>?. apply bi.sep_mono_r.
+    iApply at_bor_iff. iIntros "!> !#". iApply bi.equiv_iff.
+    apply bi.exist_proper=>?; do 7 f_equiv; first do 7 f_equiv.
+    - do 5 f_equiv. apply bi.equiv_spec; split; iApply send_change_tid.
+    - apply bi.equiv_spec; split; iApply sync_change_tid.
+    - apply bi.equiv_spec; split; iApply send_change_tid.
   Qed.
 End rwlock.
 
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 130dff9ebd6878bb8c12ee63e5c36636551591af..2287685651a262131e3f115fc24bdb0a6f698124 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -1,7 +1,7 @@
 From Coq.QArith Require Import Qcanon.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree.
-From iris.base_logic Require Import big_op fractional.
+From iris.bi Require Import fractional.
 From lrust.lang.lib Require Import memcpy.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Import typing option.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 1b0ffdc5e39cd748bf7b2977ccdcfab98458ceae..45ef6012ee5a9aa79783e17cf8d19b2848b5013a 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree.
-From iris.base_logic Require Import big_op fractional.
+From iris.bi Require Import fractional.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Import typing.
 From lrust.typing.lib.rwlock Require Import rwlock.
@@ -117,7 +117,7 @@ Section rwlockreadguard.
   Global Instance rwlockreadguard_sync α ty :
     Sync ty → Sync (rwlockreadguard α ty).
   Proof.
-    move=>?????/=. apply uPred.exist_mono=>?. by rewrite sync_change_tid.
+    move=>?????/=. apply bi.exist_mono=>?. by rewrite sync_change_tid.
   Qed.
 
   (* POSIX requires the unlock to occur from the thread that acquired
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 5bfcaccd25e7bd0b0bfc61a3a89cf1263e7f4681..c0e61e1bb822c87b52e83aaf8ffef7cf6a6bee7a 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -1,7 +1,7 @@
 From Coq.QArith Require Import Qcanon.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree.
-From iris.base_logic Require Import big_op fractional.
+From iris.bi Require Import fractional.
 From lrust.lifetime Require Import lifetime na_borrow.
 From lrust.typing Require Import typing.
 From lrust.typing.lib.rwlock Require Import rwlock rwlockreadguard.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index efb27daa4f59f26fd960c98284dab088823f25b1..b3a1b5b8736da9d0404fd7402bad7ff55b5fd5c2 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree.
-From iris.base_logic Require Import big_op fractional.
+From iris.bi Require Import fractional.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Import util typing.
 From lrust.typing.lib.rwlock Require Import rwlock.
@@ -87,7 +87,7 @@ Section rwlockwriteguard.
       iDestruct "H" as (γ β) "(Hb & #H⊑ & #Hinv & Hown)".
       iExists γ, β. iFrame "∗#". iSplit; last iSplit.
       + iApply bor_iff; last done.
-        iSplit; iIntros "!>!# H"; iDestruct "H" as (vl) "[??]";
+        iNext; iAlways; iSplit; iIntros "H"; iDestruct "H" as (vl) "[??]";
         iExists vl; iFrame; by iApply "Ho".
       + by iApply lft_incl_trans.
       + iApply at_bor_iff; try done.
@@ -120,7 +120,7 @@ Section rwlockwriteguard.
   Global Instance rwlockwriteguard_sync α ty :
     Sync ty → Sync (rwlockwriteguard α ty).
   Proof.
-    move=>?????/=. apply uPred.exist_mono=>?. do 6 f_equiv.
+    move=>?????/=. apply bi.exist_mono=>?. do 7 f_equiv.
     by rewrite sync_change_tid.
   Qed.
 
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index 509289629aa1d596bb2b74d298575a5d6236522f..9b15a6c80fd4a2b6794a03848298a243a24c76f4 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -1,7 +1,7 @@
 From Coq.QArith Require Import Qcanon.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree.
-From iris.base_logic Require Import big_op fractional.
+From iris.bi Require Import fractional.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Import typing.
 From lrust.typing.lib.rwlock Require Import rwlock rwlockwriteguard.
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index c9a91819075cc31ed63da5e779d9d07e2d20d646..32d51df55839cbf1a9abeecef43e75c9e14e36f9 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -1,5 +1,4 @@
 From iris.proofmode Require Import tactics.
-From iris.base_logic Require Import big_op.
 From lrust.lang Require Import spawn.
 From lrust.typing Require Export type.
 From lrust.typing Require Import typing.
diff --git a/theories/typing/lib/take_mut.v b/theories/typing/lib/take_mut.v
index 8d9b75a9a777faf8e4071597e8cea4416a8d11ee..2e075ad5b9fa01ddd6594bc4b1f846fa6a5dda41 100644
--- a/theories/typing/lib/take_mut.v
+++ b/theories/typing/lib/take_mut.v
@@ -1,5 +1,4 @@
 From iris.proofmode Require Import tactics.
-From iris.base_logic Require Import big_op.
 From lrust.lang.lib Require Import memcpy.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Export type.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 05fa25c25e2d47c4ce48696f3799fa72ec700d2f..d1cfa6aedfa25207f4524b68671926060a63d04c 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -1,6 +1,5 @@
 From Coq Require Import Qcanon.
 From iris.proofmode Require Import tactics.
-From iris.base_logic Require Import big_op.
 From lrust.lang.lib Require Import new_delete memcpy.
 From lrust.typing Require Export type.
 From lrust.typing Require Import util uninit type_context programs.
@@ -57,7 +56,7 @@ Section own.
 
             Since this assertion is timeless, this should not cause
             problems. *)
-           ▷ l ↦∗: ty.(ty_own) tid ∗ ▷ freeable_sz n ty.(ty_size) l
+           ▷ (l ↦∗: ty.(ty_own) tid ∗ freeable_sz n ty.(ty_size) l)
          | _ => False
          end%I;
        ty_shr κ tid l :=
@@ -72,6 +71,7 @@ Section own.
     destruct vl as [|[[|l'|]|][]];
       try (iMod (bor_persistent with "LFT Hb2 Htok") as "[>[]_]"; solve_ndisj).
     iFrame. iExists l'. rewrite heap_mapsto_vec_singleton.
+    rewrite bi.later_sep.
     iMod (bor_sep with "LFT Hb2") as "[Hb2 _]"; first solve_ndisj.
     iMod (bor_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "$"; first solve_ndisj.
     iApply delay_sharing_later; done.
@@ -203,7 +203,7 @@ Section util.
     (own_ptr n (uninit m)).(ty_own) tid [v] ⊣⊢
          ∃ (l : loc) (vl' : vec val m), ⌜v = #l⌝ ∗ ▷ l ↦∗ vl' ∗ ▷ freeable_sz n m l.
   Proof.
-    rewrite ownptr_own. apply uPred.exist_proper=>l. iSplit.
+    rewrite ownptr_own. apply bi.exist_proper=>l. iSplit.
     (* FIXME: The goals here look rather confusing:  One cannot tell that we are looking at
        a statement in Iris; the top-level → could just as well be a Coq implication. *)
     - iIntros "H". iDestruct "H" as (vl) "(% & Hl & _ & $)". subst v.
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 525c039cd1d73a3dd84550cb50ad670556d2b45e..8130c5aedd2385fd4650d2049abb323c4aec0821 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -1,6 +1,5 @@
 From Coq Require Import Qcanon.
 From iris.proofmode Require Import tactics.
-From iris.base_logic Require Import big_op.
 From lrust.typing Require Export type.
 From lrust.typing Require Import type_context lft_contexts product own uniq_bor shr_bor.
 Set Default Proof Using "Type".
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 755256c0cd1766a1b020539082ab1217aa6eb9aa..5a298fa46afc71aec62e1a78a1ce1acc683efcab 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -1,4 +1,3 @@
-From iris.base_logic Require Import big_op.
 From lrust.lang Require Import proofmode memcpy.
 From lrust.typing Require Export type lft_contexts type_context cont_context.
 Set Default Proof Using "Type".
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 3d4bfc702d53d650ca1e5b93221ccd02a722fe52..7d8363539cdfedd3b32561adc9c251b64079fc20 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -1,4 +1,3 @@
-From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
 From lrust.typing Require Export type.
 From lrust.typing Require Import lft_contexts type_context programs.
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index cc98e8b4ecd2cd380b6038dcda9ba329c32eb59f..e35c3b5034580811456ef87f7fefe4e7b9329daa 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -1,5 +1,4 @@
 From iris.algebra Require Import frac.
-From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import na_invariants.
 From iris.proofmode Require Import tactics.
 From lrust.lang Require Import races adequacy proofmode notation.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 107c3b0437d99613ef7ffb34ce55ba7b38bac8d6..c7915072011224da9145308e5c944664f3bee69a 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -1,7 +1,6 @@
-From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import list.
-From iris.base_logic Require Import fractional.
+From iris.bi Require Import fractional.
 From lrust.typing Require Export type.
 Set Default Proof Using "Type".
 
@@ -231,9 +230,9 @@ Section sum.
     iIntros (????) "[]".
   Qed.
 
-  Definition emp := sum [].
+  Definition emp_type := sum [].
 
-  Global Instance emp_empty : Empty type := emp.
+  Global Instance emp_type_empty : Empty type := emp_type.
 End sum.
 
 (* Σ is commonly used for the current functor. So it cannot be defined
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 34fb8dd997c3e564805114ee2975ff8b833788b3..7dd9169bf6bc77bbb8118691c110cac2ed326f40 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -1,5 +1,4 @@
 From iris.base_logic.lib Require Export na_invariants.
-From iris.base_logic Require Import big_op.
 From lrust.lang Require Export proofmode notation.
 From lrust.lifetime Require Export frac_borrow.
 From lrust.typing Require Export base.
@@ -215,10 +214,10 @@ Section ofe.
     - by intros [].
     - (* TODO: automate this *)
       repeat apply limit_preserving_and; repeat (apply limit_preserving_forall; intros ?).
-      + apply uPred.limit_preserving_Persistent=> n ty1 ty2 Hty; apply Hty.
-      + apply uPred.limit_preserving_entails=> n ty1 ty2 Hty. apply Hty. by rewrite Hty.
-      + apply uPred.limit_preserving_entails=> n ty1 ty2 Hty; repeat f_equiv; apply Hty.
-      + apply uPred.limit_preserving_entails=> n ty1 ty2 Hty; repeat f_equiv; apply Hty.
+      + apply bi.limit_preserving_Persistent=> n ty1 ty2 Hty; apply Hty.
+      + apply bi.limit_preserving_entails=> n ty1 ty2 Hty. apply Hty. by rewrite Hty.
+      + apply bi.limit_preserving_entails=> n ty1 ty2 Hty; repeat f_equiv; apply Hty.
+      + apply bi.limit_preserving_entails=> n ty1 ty2 Hty; repeat f_equiv; apply Hty.
   Qed.
 
   Inductive st_equiv' (ty1 ty2 : simple_type) : Prop :=
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index aa8796768ea53dfa3d640e8a23548423e43255e0..6b3e7e722b90113cc5efd9029406b341d763590a 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -1,5 +1,4 @@
 From iris.proofmode Require Import tactics.
-From iris.base_logic Require Import big_op.
 From lrust.typing Require Import type lft_contexts.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index ec9013bd384e88e5bb71b2b7bed7bf7812a8ac75..eb07fa950860ac8c5d53cd14114ea84c1473576a 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -1,5 +1,4 @@
 From iris.proofmode Require Import tactics.
-From iris.base_logic Require Import big_op.
 From lrust.lang Require Import heap.
 From lrust.typing Require Export type.
 From lrust.typing Require Import util lft_contexts type_context programs.
@@ -55,7 +54,7 @@ Section uniq_bor.
     iSpecialize ("Hκ" with "HE"). iSplit; iAlways.
     - iIntros (? [|[[]|][]]) "H"; try done.
       iApply (bor_shorten with "Hκ"). iApply bor_iff; last done.
-      iSplit; iIntros "!>!# H"; iDestruct "H" as (vl) "[??]";
+      iNext. iAlways. iSplit; iIntros "H"; iDestruct "H" as (vl) "[??]";
       iExists vl; iFrame; by iApply "Ho".
     - iIntros (κ ??) "H". iAssert (κ2 ⊓ κ ⊑ κ1 ⊓ κ)%I as "#Hincl'".
       { iApply lft_intersect_mono. done. iApply lft_incl_refl. }
@@ -82,7 +81,7 @@ Section uniq_bor.
     Send ty → Send (uniq_bor κ ty).
   Proof.
     iIntros (Hsend tid1 tid2 [|[[]|][]]) "H"; try done.
-    iApply bor_iff; last done. iNext. iAlways. iApply uPred.equiv_iff.
+    iApply bor_iff; last done. iNext. iAlways. iApply bi.equiv_iff.
     do 3 f_equiv. iSplit; iIntros "."; by iApply Hsend.
   Qed.