diff --git a/opam b/opam
index c0971646ea91ea08f80ace314560e429e1428f41..fd87ed868f41c568695dabdc021176b8b850d41c 100644
--- a/opam
+++ b/opam
@@ -14,7 +14,7 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2020-07-15.1.6ae02201") | (= "dev") }
+  "coq-iris" { (= "dev.2020-07-22.0.1e8432a9") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index 203abf73b5818245e22b44f873c2294c43eb4c37..67b0837422fbcdff7f9a07c2ed3f49d81a9fca8c 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -268,25 +268,25 @@ Section arc.
     iModIntro. wp_let. wp_op. wp_bind (CAS _ _ _). iInv N as (st) "[>H● H]" "Hclose1".
     iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
     iDestruct (arc_tok_auth_val with "H● Hown") as %(?&strong'&?&?&[-> _]).
-    iDestruct "H" as (q) "(>#Hq & [HP1 HP1'] & Hl & Hw)". iDestruct "Hq" as %Hq.
+    iDestruct "H" as (qq) "(>#Hq & [HP1 HP1'] & Hl & Hw)". iDestruct "Hq" as %Hq.
     destruct (decide (strong = strong')) as [->|?].
     - wp_apply (wp_cas_int_suc with "Hl"). iIntros "Hl".
       iMod (own_update with "H●") as "[H● Hown']".
       { apply auth_update_alloc, prod_local_update_1,
-         (op_local_update_discrete _ _ (Some (Cinl ((q/2)%Qp, 1%positive, None))))
+         (op_local_update_discrete _ _ (Some (Cinl ((qq/2)%Qp, 1%positive, None))))
            =>-[/= Hqa ?]. split;[split|]=>//=; last by rewrite left_id.
-        apply frac_valid'. rewrite -Hq comm_L -{2}(Qp_div_2 q).
+        apply frac_valid'. rewrite -Hq comm_L -{2}(Qp_div_2 qq).
         apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (_ / _)%Qp).
         apply Qcplus_le_mono_r, Qp_ge_0. }
       iMod ("Hclose2" with "Hown") as "HP". iModIntro.
       iMod ("Hclose1" with "[Hl Hw H● HP1']") as "_".
       { iExists _. iFrame. iExists _. rewrite /= [xH ⋅ _]comm_L. iFrame.
-        rewrite [(q / 2)%Qp ⋅ _]comm frac_op' -[(_ + _)%Qp]assoc Qp_div_2 left_id_L. auto. }
+        rewrite [(qq / 2)%Qp ⋅ _]comm frac_op' -[(_ + _)%Qp]assoc Qp_div_2 left_id_L. auto. }
       iModIntro. wp_case. iApply "HΦ". iFrame.
     - wp_apply (wp_cas_int_fail with "Hl"); [congruence|]. iIntros "Hl".
       iMod ("Hclose2" with "Hown") as "HP". iModIntro.
       iMod ("Hclose1" with "[-HP HΦ]") as "_".
-      { iExists _. iFrame. iExists q. auto with iFrame. }
+      { iExists _. iFrame. iExists qq. auto with iFrame. }
       iModIntro. wp_case. iApply ("IH" with "HP HΦ").
   Qed.
 
@@ -309,7 +309,7 @@ Section arc.
     iApply fupd_wp. iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
     iDestruct (arc_tok_auth_val with "H● Hown") as %(?&?& wlock & weak' &[-> _]).
     iMod ("Hclose2" with "Hown") as "HP". iModIntro.
-    iDestruct "H" as (q) "(>Heq & HP1 & Hl & Hl1)". iDestruct "Heq" as %Heq.
+    iDestruct "H" as (qq) "(>Heq & HP1 & Hl & Hl1)". iDestruct "Heq" as %Heq.
     destruct (decide (weak = weak' ∧ wlock = None)) as [[<- ->]|Hw].
     - wp_apply (wp_cas_int_suc with "Hl1"). iIntros "Hl1".
       iMod (own_update with "H●") as "[H● Hown']".
@@ -509,7 +509,7 @@ Section arc.
     iIntros "#INV !# * [Hown HP1] HΦ". iLöb as "IH".
     wp_rec. wp_bind (!ˢᶜ_)%E. iInv N as (st) "[>H● H]" "Hclose".
     iDestruct (arc_tok_auth_val with "H● Hown") as %(?& s &?&?&[-> _]).
-    iDestruct "H" as (?) "(? & ? & ? & ?)". wp_read.
+    iDestruct "H" as (x') "(? & ? & ? & ?)". wp_read.
     iMod ("Hclose" with "[-Hown HP1 HΦ]") as "_". { iExists _. auto with iFrame. }
     iModIntro. wp_let. wp_op. wp_bind (CAS _ _ _). iInv N as (st) "[>H● H]" "Hclose".
     iDestruct (arc_tok_auth_val with "H● Hown") as %(q' & s' & wl & w &[-> Hqq']).
diff --git a/theories/lang/lib/lock.v b/theories/lang/lib/lock.v
index 0d50e7ceb9aa4adf2f18f15ed4387eae46f66a12..321a07895aad959861d3f0db3c2ea7e2d8650412 100644
--- a/theories/lang/lib/lock.v
+++ b/theories/lang/lib/lock.v
@@ -36,7 +36,7 @@ Section proof.
   Proof.
     iIntros "#HR !#". iSplit; iIntros "Hlck"; iApply (lock_proto_iff with "[HR] Hlck").
     - done.
-    - iAlways; iSplit; iIntros; by iApply "HR".
+    - iModIntro; iSplit; iIntros; by iApply "HR".
   Qed.
 
   (** The main proofs. *)
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index 3b0aa996b1ef3a8040f57b2ec5c4817d7ac439e9..b6bff0b005a8cd1b65e9335fc25c72e6e1d510bc 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -140,7 +140,7 @@ Lemma wp_alloc E (n : Z) :
   {{{ l (sz: nat), RET LitV $ LitLoc l; ⌜n = sz⌝ ∗ †l…sz ∗ l ↦∗ repeat (LitV LitPoison) sz }}}.
 Proof.
   iIntros (? Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 ???) "Hσ !>"; iSplit; first by auto.
+  iIntros (σ1 κ κs n') "Hσ !>"; iSplit; first by auto.
   iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
   iMod (heap_alloc with "Hσ") as "[Hσ Hl]"; [done..|].
   iModIntro; iSplit=> //. iFrame.
@@ -154,7 +154,7 @@ Lemma wp_free E (n:Z) l vl :
   {{{ RET LitV LitPoison; True }}}.
 Proof.
   iIntros (? Φ) "[>Hmt >Hf] HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 ???) "Hσ".
+  iIntros (σ1 κ κs n') "Hσ".
   iMod (heap_free _ _ _ n with "Hσ Hmt Hf") as "(% & % & Hσ)"=>//.
   iModIntro; iSplit; first by auto.
   iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
@@ -166,7 +166,7 @@ Lemma wp_read_sc E l q v :
   {{{ RET v; l ↦{q} v }}}.
 Proof.
   iIntros (?) ">Hv HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 ???) "Hσ". iDestruct (heap_read with "Hσ Hv") as %[n ?].
+  iIntros (σ1 κ κs n) "Hσ". iDestruct (heap_read with "Hσ Hv") as %[m ?].
   iModIntro; iSplit; first by eauto.
   iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
@@ -176,15 +176,15 @@ Lemma wp_read_na E l q v :
   {{{ ▷ l ↦{q} v }}} Read Na1Ord (Lit $ LitLoc l) @ E
   {{{ RET v; l ↦{q} v }}}.
 Proof.
-  iIntros (Φ) ">Hv HΦ". iApply wp_lift_head_step; auto. iIntros (σ1 ???) "Hσ".
-  iMod (heap_read_na with "Hσ Hv") as (n) "(% & Hσ & Hσclose)".
+  iIntros (Φ) ">Hv HΦ". iApply wp_lift_head_step; auto. iIntros (σ1 κ κs n) "Hσ".
+  iMod (heap_read_na with "Hσ Hv") as (m) "(% & Hσ & Hσclose)".
   iMod (fupd_intro_mask' _ ∅) as "Hclose"; first set_solver.
   iModIntro; iSplit; first by eauto.
   iNext; iIntros (e2 σ2 efs Hstep); inv_head_step. iMod "Hclose" as "_".
   iModIntro. iFrame "Hσ". iSplit; last done.
   clear dependent σ1 n.
   iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 ???) "Hσ". iMod ("Hσclose" with "Hσ") as (n) "(% & Hσ & Hv)".
+  iIntros (σ1 κ' κs' n') "Hσ". iMod ("Hσclose" with "Hσ") as (n) "(% & Hσ & Hv)".
   iModIntro; iSplit; first by eauto.
   iNext; iIntros (e2 σ2 efs Hstep) "!>"; inv_head_step.
   iFrame "Hσ". iSplit; [done|]. by iApply "HΦ".
@@ -196,7 +196,7 @@ Lemma wp_write_sc E l e v v' :
   {{{ RET LitV LitPoison; l ↦ v }}}.
 Proof.
   iIntros (<- Φ) ">Hv HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 ???) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
+  iIntros (σ1 κ κs n) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
   iMod (heap_write _ _ _  v with "Hσ Hv") as "[Hσ Hv]".
   iModIntro; iSplit; first by eauto.
   iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
@@ -209,14 +209,14 @@ Lemma wp_write_na E l e v v' :
   {{{ RET LitV LitPoison; l ↦ v }}}.
 Proof.
   iIntros (<- Φ) ">Hv HΦ".
-  iApply wp_lift_head_step; auto. iIntros (σ1 ???) "Hσ".
+  iApply wp_lift_head_step; auto. iIntros (σ1 κ κs n) "Hσ".
   iMod (heap_write_na with "Hσ Hv") as "(% & Hσ & Hσclose)".
   iMod (fupd_intro_mask' _ ∅) as "Hclose"; first set_solver.
   iModIntro; iSplit; first by eauto.
   iNext; iIntros (e2 σ2 efs Hstep); inv_head_step. iMod "Hclose" as "_".
   iModIntro. iFrame "Hσ". iSplit; last done.
   clear dependent σ1. iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 ???) "Hσ". iMod ("Hσclose" with "Hσ") as "(% & Hσ & Hv)".
+  iIntros (σ1 κ' κs' n') "Hσ". iMod ("Hσclose" with "Hσ") as "(% & Hσ & Hv)".
   iModIntro; iSplit; first by eauto.
   iNext; iIntros (e2 σ2 efs Hstep) "!>"; inv_head_step.
   iFrame "Hσ". iSplit; [done|]. by iApply "HΦ".
@@ -230,7 +230,7 @@ Lemma wp_cas_int_fail E l q z1 e2 lit2 zl :
 Proof.
   iIntros (<- ? Φ) ">Hv HΦ".
   iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 ???) "Hσ". iDestruct (heap_read with "Hσ Hv") as %[n ?].
+  iIntros (σ1 κ κs n) "Hσ". iDestruct (heap_read with "Hσ Hv") as %[m ?].
   iModIntro; iSplit; first by eauto.
   iNext; iIntros (v2 σ2 efs Hstep); inv_head_step; inv_lit.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
@@ -244,7 +244,7 @@ Lemma wp_cas_suc E l lit1 e2 lit2 :
 Proof.
   iIntros (<- ? Φ) ">Hv HΦ".
   iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 ???) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
+  iIntros (σ1 κ κs n) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
   iModIntro; iSplit; first (destruct lit1; by eauto).
   iNext; iIntros (v2 σ2 efs Hstep); inv_head_step; [inv_lit|].
   iMod (heap_write with "Hσ Hv") as "[$ Hv]".
@@ -274,7 +274,7 @@ Lemma wp_cas_loc_fail E l q q' q1 l1 v1' e2 lit2 l' vl' :
 Proof.
   iIntros (<- ? Φ) "(>Hl & >Hl' & >Hl1) HΦ".
   iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 ???) "Hσ". iDestruct (heap_read with "Hσ Hl") as %[nl ?].
+  iIntros (σ1 κ κs n) "Hσ". iDestruct (heap_read with "Hσ Hl") as %[nl ?].
   iDestruct (heap_read with "Hσ Hl'") as %[nl' ?].
   iDestruct (heap_read with "Hσ Hl1") as %[nl1 ?].
   iModIntro; iSplit; first by eauto.
@@ -292,7 +292,7 @@ Lemma wp_cas_loc_nondet E l l1 e2 l2 ll :
 Proof.
   iIntros (<- Φ) ">Hv HΦ".
   iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 ???) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
+  iIntros (σ1 κ κs n) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
   iModIntro; iSplit; first (destruct (decide (ll = l1)) as [->|]; by eauto).
   iNext; iIntros (v2 σ2 efs Hstep); inv_head_step; last lia.
   - inv_lit. iModIntro; iSplit; [done|]; iFrame "Hσ".
@@ -313,7 +313,7 @@ Proof.
       [done|solve_exec_safe|solve_exec_puredet|].
     iApply wp_value. by iApply Hpost.
   - iApply wp_lift_atomic_head_step_no_fork; subst=>//.
-    iIntros (σ1 ???) "Hσ1". iModIntro. inv_head_step.
+    iIntros (σ1 κ κs n') "Hσ1". iModIntro. inv_head_step.
     iSplitR.
     { iPureIntro. repeat eexists. econstructor. eapply BinOpEqFalse. by auto. }
     (* We need to do a little gymnastics here to apply Hne now and strip away a
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index e844bbda3abfce60326e2c44efcbaa205123d768..e666a1305bb81de8868da6781f3d5efe8414692a 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -30,7 +30,7 @@ Section frac_bor.
     ▷ □ (∀ q, φ q ↔ φ' q) -∗ &frac{κ} φ -∗ &frac{κ} φ'.
   Proof.
     iIntros "#Hφφ' H". iDestruct "H" as (γ κ') "[? Hφ]". iExists γ, κ'. iFrame.
-    iApply (at_bor_iff with "[Hφφ'] Hφ"). iNext. iAlways.
+    iApply (at_bor_iff with "[Hφφ'] Hφ"). iNext. iModIntro.
     iSplit; iIntros "H"; iDestruct "H" as (q) "[H ?]"; iExists q; iFrame; by iApply "Hφφ'".
   Qed.
 
@@ -137,7 +137,7 @@ End frac_bor.
 Lemma frac_bor_lft_incl `{!invG Σ, !lftG Σ, !frac_borG Σ} κ κ' q:
   lft_ctx -∗ &frac{κ}(λ q', (q * q').[κ']) -∗ κ ⊑ κ'.
 Proof.
-  iIntros "#LFT#Hbor". iApply lft_incl_intro. iAlways. iSplitR.
+  iIntros "#LFT#Hbor". iApply lft_incl_intro. iModIntro. iSplitR.
   - iIntros (q') "Hκ'".
     iMod (frac_bor_acc with "LFT Hbor Hκ'") as (q'') "[>? Hclose]". done.
     iExists _. iFrame. iIntros "!>Hκ'". iApply "Hclose". auto.
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index 13271eb54c3193b86f2d28b1c0572cbebc20f836..ae9358d09961adbdba739339d0fdbd81e81a6dfc 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -111,7 +111,7 @@ Qed.
 Lemma bor_iff_proper κ P P': ▷ □ (P ↔ P') -∗ □ (&{κ}P ↔ &{κ}P').
 Proof.
   iIntros "#HP !#". iSplit; iIntros "?"; iApply bor_iff; try done.
-  iNext. iAlways. iSplit; iIntros "?"; iApply "HP"; done.
+  iNext. iModIntro. iSplit; iIntros "?"; iApply "HP"; done.
 Qed.
 
 Lemma bor_later E κ P :
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index 61471b2ba8cb67ff73c113538194303d7e6fb10c..3f17636a0eaa98339be220a992f887f7375420f9 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -120,7 +120,7 @@ Proof.
     iAssert (&{κ}(P ∗ Q))%I with "[H◯ Hslice]" as "$".
     { rewrite /bor /raw_bor /idx_bor_own. iExists (κ1 ⊓ κ2).
       iSplit; first by iApply (lft_incl_glb with "Hκ1 Hκ2").
-      iExists γ. iFrame. iExists _. iFrame. iNext. iAlways.
+      iExists γ. iFrame. iExists _. iFrame. iNext. iModIntro.
       by iSplit; iIntros "[HP HQ]"; iSplitL "HP"; (iApply "HPP'" || iApply "HQQ'"). }
     iApply "Hclose". iExists A, I. iFrame. rewrite big_sepS_later.
     iApply "Hclose'". iLeft. iFrame "%". iExists Pb, Pi. iFrame. iExists _.
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index b9b2fbeea4b68676ffa3b89893425eaa87ee33e2..f74160d118d90efd43102d29d95fd1878fa3df9a 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -71,7 +71,7 @@ Proof.
   pose (Kalive := filter (lft_alive_in A) K).
   destruct (decide (Kalive = ∅)) as [HKalive|].
   { iModIntro. rewrite /Iinv. iFrame.
-    iApply (@big_sepS_impl with "[$HK]"); iAlways.
+    iApply (@big_sepS_impl with "[$HK]"); iModIntro.
     rewrite /lft_inv. iIntros (κ Hκ) "[[[_ %]|[$ _]] _]". set_solver. }
   destruct (minimal_exists_L (⊂) Kalive)
     as (κ & [Hκalive HκK]%elem_of_filter & Hκmin); first done.
@@ -122,7 +122,7 @@ Proof.
   { iNext. rewrite /lfts_inv /own_alft_auth.
     iExists (<[Λ:=true]>A), I. rewrite /to_alftUR fmap_insert; iFrame.
     iApply (@big_sepS_impl with "[$Hinv]").
-    iAlways. rewrite /lft_inv. iIntros (κ ?) "[[Hκ %]|[Hκ %]]".
+    iModIntro. rewrite /lft_inv. iIntros (κ ?) "[[Hκ %]|[Hκ %]]".
     - iLeft. iFrame "Hκ". iPureIntro. by apply lft_alive_in_insert.
     - iRight. iFrame "Hκ". iPureIntro. by apply lft_dead_in_insert. }
   iModIntro; iExists {[ Λ ]}.
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 8d7d0ddf09c458831b824bde251154e73a67c8eb..390bf7aee6646b0da8c03dcdd9f1f7f34ebafc07 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -386,14 +386,14 @@ Lemma raw_bor_iff i P P' : ▷ □ (P ↔ P') -∗ raw_bor i P -∗ raw_bor i P'
 Proof.
   iIntros "#HPP' HP". unfold raw_bor. iDestruct "HP" as (s) "[HiP HP]".
   iExists s. iFrame. iDestruct "HP" as (P0) "[#Hiff ?]". iExists P0. iFrame.
-  iNext. iAlways. iSplit; iIntros.
+  iNext. iModIntro. iSplit; iIntros.
   by iApply "HPP'"; iApply "Hiff". by iApply "Hiff"; iApply "HPP'".
 Qed.
 
 Lemma idx_bor_iff κ i P P' : ▷ □ (P ↔ P') -∗ &{κ,i}P -∗ &{κ,i}P'.
 Proof.
   unfold idx_bor. iIntros "#HPP' [$ HP]". iDestruct "HP" as (P0) "[#HP0P Hs]".
-  iExists P0. iFrame. iNext. iAlways. iSplit; iIntros.
+  iExists P0. iFrame. iNext. iModIntro. iSplit; iIntros.
   by iApply "HPP'"; iApply "HP0P". by iApply "HP0P"; iApply "HPP'".
 Qed.
 
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 209a50a541857f191be7738c82327b12e0729d2e..1dd2d629f03ef6b86ff1034bc21868e8a0680651 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -276,7 +276,7 @@ Section typing.
       + iApply "HE'". iIntros "{$# Hf Hinh HE' LFT HE %}".
         iInduction κs as [|κ κs] "IH"=> //=. iSplitL.
         { iApply lft_incl_trans; first done. iApply lft_intersect_incl_l. }
-        iApply "IH". iAlways. iApply lft_incl_trans; first done.
+        iApply "IH". iModIntro. iApply lft_incl_trans; first done.
         iApply lft_intersect_incl_r.
       + iSplitL; last done. iExists ϝ. iSplit; first by rewrite /= left_id.
         iFrame "#∗".
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 627bd6a48fb6a2696286975647bd81e0b3b81048..b7ac9370e30149c69221cf8b516ee132805984ce 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -151,7 +151,7 @@ Section arc.
   Next Obligation.
     iIntros (ty κ κ' tid l) "#Hincl H". iDestruct "H" as (l') "[#Hl #Hshr]".
     iExists _. iSplit; first by iApply frac_bor_shorten.
-    iAlways. iIntros (F q) "% Htok".
+    iModIntro. iIntros (F q) "% Htok".
     iMod (lft_incl_acc with "Hincl Htok") as (q'') "[Htok Hclose]"; first solve_ndisj.
     iMod ("Hshr" with "[] Htok") as "Hshr2"; first done.
     iModIntro. iNext. iMod "Hshr2" as "[Htok HX]".
@@ -178,7 +178,7 @@ Section arc.
     type_incl ty1 ty2 -∗ type_incl (arc ty1) (arc ty2).
   Proof.
     iIntros "#Hincl". iPoseProof "Hincl" as "(#Hsz & #Hoincl & #Hsincl)".
-    iSplit; first done. iSplit; iAlways.
+    iSplit; first done. iSplit; iModIntro.
     - iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
       iDestruct "Hvl" as "[(Hl1 & Hl2 & H† & Hc) | Hvl]".
       { iLeft. iFrame. iDestruct "Hsz" as %->.
@@ -266,7 +266,7 @@ Section arc.
   Next Obligation.
     iIntros (ty κ κ' tid l) "#Hincl H". iDestruct "H" as (l') "[#Hl #Hshr]".
     iExists _. iSplit; first by iApply frac_bor_shorten.
-    iAlways. iIntros (F q) "% Htok".
+    iModIntro. iIntros (F q) "% Htok".
     iMod (lft_incl_acc with "Hincl Htok") as (q'') "[Htok Hclose]"; first solve_ndisj.
     iMod ("Hshr" with "[] Htok") as "Hshr2"; first done.
     iModIntro. iNext. iMod "Hshr2" as "[Htok HX]".
@@ -291,7 +291,7 @@ Section arc.
     type_incl ty1 ty2 -∗ type_incl (weak ty1) (weak ty2).
   Proof.
     iIntros "#Hincl". iPoseProof "Hincl" as "(#Hsz & #Hoincl & #Hsincl)".
-    iSplit; first done. iSplit; iAlways.
+    iSplit; first done. iSplit; iModIntro.
     - iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
       iDestruct "Hvl" as (γ ν) "(#Hpersist & Htk)".
       iExists _, _. iFrame "#∗". by iApply arc_persist_type_incl.
@@ -783,9 +783,9 @@ Section arc.
       { iIntros "_". wp_if. unlock. iFrame. iExists (_::_). rewrite heap_mapsto_vec_cons.
         iFrame. iExists 1%nat, _, []. rewrite /= right_id_L Max.max_0_r.
         auto 10 with iFrame. }
-      iIntros "([H† H1] & H2 & H3)". iDestruct "H1" as (vl') "[H1 Heq]".
+      iIntros "([H† H1] & H2 & H3)". iDestruct "H1" as (vl1) "[H1 Heq]".
       iDestruct "Heq" as %<-. wp_if.
-      wp_apply (wp_delete _ _ _ (_::_::vl') with "[H1 H2 H3 H†]").
+      wp_apply (wp_delete _ _ _ (_::_::vl1) with "[H1 H2 H3 H†]").
       { simpl. lia. }
       { rewrite 2!heap_mapsto_vec_cons shift_loc_assoc. auto with iFrame. }
       iFrame. iIntros "_". iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame.
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 1cdd3aabe3cd532b1e80ca160f1926b962a6f14a..ca2dc5ca6f4bc9f518fba5e1e1ade8698c13613b 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -39,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. iNext; iAlways; iSplit; iIntros "H";
+    - iApply na_bor_iff; last done. iNext; iModIntro; 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/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index e1935d628cf1279b0bff941de89b189786902db1..72e08c6d60fa19549f023ade400572bbe30a0fd8 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -101,7 +101,7 @@ Section mutex.
       iExists _. iFrame "Hincl". iApply (at_bor_iff with "[] Hshr"). iNext.
       iApply lock_proto_iff_proper. iApply bor_iff_proper. iNext.
       iApply heap_mapsto_pred_iff_proper.
-      iAlways; iIntros; iSplit; iIntros; by iApply "Howni".
+      iModIntro; iIntros; iSplit; iIntros; by iApply "Howni".
   Qed.
 
   Global Instance mutex_proper E L :
@@ -122,7 +122,7 @@ Section mutex.
     iExists _. iFrame "Hincl". iApply (at_bor_iff with "[] Hshr"). iNext.
     iApply lock_proto_iff_proper. iApply bor_iff_proper. iNext.
     iApply heap_mapsto_pred_iff_proper.
-    iAlways; iIntros; iSplit; iIntros; by iApply send_change_tid.
+    iModIntro; iIntros; iSplit; iIntros; by iApply send_change_tid.
   Qed.
 End mutex.
 
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index d0f2e34e39f0c4892a7bbfaa7a6a26fc6f196e5e..cbd04b88f7c320a29d74b4f4c5a7806bc5036d80 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -91,7 +91,7 @@ Section mguard.
     intros α1 α2 Hα ty1 ty2 Hty. generalize Hty. rewrite eqtype_unfold. iIntros (Hty' q) "HL".
     iDestruct (Hty' with "HL") as "#Hty". clear Hty'. iDestruct (Hα with "HL") as "#Hα".
     iIntros "!# #HE". iDestruct ("Hα" with "HE") as "{Hα} Hα".
-    iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs) {HE Hty}". iSplit; [done|iSplit; iAlways].
+    iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs) {HE Hty}". iSplit; [done|iSplit; iModIntro].
     - iIntros (tid [|[[]|][]]) "H"; try done. simpl.
       iDestruct "H" as (β) "(#H⊑ & #Hinv & Hown)".
       iExists β. iFrame. iSplit; last iSplit.
@@ -100,10 +100,10 @@ Section mguard.
         iApply (at_bor_iff with "[] Hinv"). iNext.
         iApply lock_proto_iff_proper. iApply bor_iff_proper. iNext.
         iApply heap_mapsto_pred_iff_proper.
-        iAlways; iIntros; iSplit; iIntros; by iApply "Ho".
+        iModIntro; iIntros; iSplit; iIntros; by iApply "Ho".
       + iApply bor_iff; last done. iNext.
         iApply heap_mapsto_pred_iff_proper.
-        iAlways; iIntros; iSplit; iIntros; by iApply "Ho".
+        iModIntro; iIntros; iSplit; iIntros; by iApply "Ho".
     - iIntros (κ tid l) "H". iDestruct "H" as (l') "H". iExists l'.
       iDestruct "H" as "[$ #H]". iIntros "!# * % Htok".
       iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 36eadb4f851e29a0a9dfd757ae5e1b66437a73da..e017caaf49fb345ba2e6ed3a0fd03513f7bfed81 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -184,7 +184,7 @@ Section rc.
   Next Obligation.
     iIntros (ty κ κ' tid l) "#Hincl H". iDestruct "H" as (l') "[#Hl #Hshr]".
     iExists _. iSplit; first by iApply frac_bor_shorten.
-    iAlways. iIntros (F q) "% Htok".
+    iModIntro. iIntros (F q) "% Htok".
     iMod (lft_incl_acc with "Hincl Htok") as (q'') "[Htok Hclose]"; first solve_ndisj.
     iMod ("Hshr" with "[] Htok") as "Hshr2"; first done.
     iModIntro. iNext. iMod "Hshr2" as "[Htok HX]".
@@ -211,7 +211,7 @@ Section rc.
     type_incl ty1 ty2 -∗ type_incl (rc ty1) (rc ty2).
   Proof.
     iIntros "#Hincl". iPoseProof "Hincl" as "(#Hsz & #Hoincl & #Hsincl)".
-    iSplit; first done. iSplit; iAlways.
+    iSplit; first done. iSplit; iModIntro.
     - iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
       iDestruct "Hvl" as "[(Hl1 & Hl2 & H† & Hc) | Hvl]".
       { iLeft. iFrame. iDestruct "Hsz" as %->.
@@ -689,7 +689,7 @@ Section code.
     iApply (type_cont [] [ϝ ⊑ₗ []]
                       (λ _, [rcx ◁ box (uninit 1); r ◁ box (Σ[ ty; rc ty ])])) ;
       [solve_typing..| |]; last first.
-    { simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
+    { simpl. iModIntro. iIntros (k arg). inv_vec arg. simpl_subst.
       iApply type_delete; [solve_typing..|].
       iApply type_jump; solve_typing. }
     iIntros (k). simpl_subst.
@@ -784,7 +784,7 @@ Section code.
     iApply (type_cont [] [ϝ ⊑ₗ []]
                       (λ _, [rcx ◁ box (uninit 1); r ◁ box (option ty)]));
       [solve_typing..| |]; last first.
-    { simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
+    { simpl. iModIntro. iIntros (k arg). inv_vec arg. simpl_subst.
       iApply type_delete; [solve_typing..|].
       iApply type_jump; solve_typing. }
     iIntros (k). simpl_subst.
@@ -874,7 +874,7 @@ Section code.
     iApply (type_cont [] [ϝ ⊑ₗ []]
                       (λ _, [rcx ◁ box (uninit 1); r ◁ box (option $ &uniq{α}ty)]));
       [solve_typing..| |]; last first.
-    { simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
+    { simpl. iModIntro. iIntros (k arg). inv_vec arg. simpl_subst.
       iApply type_delete; [solve_typing..|].
       iApply type_jump; solve_typing. }
     iIntros (k). simpl_subst.
@@ -1006,7 +1006,7 @@ Section code.
     iApply (type_cont [] [ϝ ⊑ₗ []]
                       (λ _, [rcx ◁ box (uninit 1); r ◁ box (&uniq{α}ty)]));
       [solve_typing..| |]; last first.
-    { simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
+    { simpl. iModIntro. iIntros (k arg). inv_vec arg. simpl_subst.
       iApply type_delete; [solve_typing..|].
       iApply type_jump; solve_typing. }
     iIntros (k). simpl_subst.
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 9680aee6b6b6c30aacccaf050bdc06b28b0d25a9..6c3e1e05fc6126821c54b82b133f53b491f04f19 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -57,7 +57,7 @@ Section weak.
   Next Obligation.
     iIntros (ty κ κ' tid l) "#Hincl H". iDestruct "H" as (l') "[#Hl #Hshr]".
     iExists _. iSplit; first by iApply frac_bor_shorten.
-    iAlways. iIntros (F q) "% Htok".
+    iModIntro. iIntros (F q) "% Htok".
     iMod (lft_incl_acc with "Hincl Htok") as (q'') "[Htok Hclose]"; first solve_ndisj.
     iMod ("Hshr" with "[] Htok") as "Hshr2"; first done.
     iModIntro. iNext. iMod "Hshr2" as "[Htok HX]".
@@ -82,7 +82,7 @@ Section weak.
     type_incl ty1 ty2 -∗ type_incl (weak ty1) (weak ty2).
   Proof.
     iIntros "#Hincl". iPoseProof "Hincl" as "(Hsz & #Hoincl & #Hsincl)".
-    iSplit; first done. iSplit; iAlways.
+    iSplit; first done. iSplit; iModIntro.
     - iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
       iDestruct "Hvl" as (γ ν) "(#Hpersist & Htok)".
       iExists _, _. iFrame "Htok". by iApply rc_persist_type_incl.
@@ -132,7 +132,7 @@ Section code.
     iApply (type_cont [] [ϝ ⊑ₗ []]
                       (λ _, [w ◁ box (&shr{α}(weak ty)); r ◁ box (option (rc ty))])) ;
       [solve_typing..| |]; last first.
-    { simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
+    { simpl. iModIntro. iIntros (k arg). inv_vec arg. simpl_subst.
       iApply type_delete; [solve_typing..|].
       iApply type_jump; solve_typing. }
     iIntros (k). simpl_subst.
@@ -380,7 +380,7 @@ Section code.
     iIntros (_ ϝ ret arg). inv_vec arg=>w. simpl_subst.
     iApply (type_cont [] [ϝ ⊑ₗ []] (λ _, [w ◁ box (uninit 1)]));
       [solve_typing..| |]; last first.
-    { simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
+    { simpl. iModIntro. iIntros (k arg). inv_vec arg. simpl_subst.
       iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
       iApply type_delete; [solve_typing..|].
       iApply type_jump; solve_typing. }
diff --git a/theories/typing/lib/refcell/ref.v b/theories/typing/lib/refcell/ref.v
index 6f403685929c2415cb193e6d41a2f0b4c636bc1d..108291c45bf33f41bbe42633acd5ca962f0645d7 100644
--- a/theories/typing/lib/refcell/ref.v
+++ b/theories/typing/lib/refcell/ref.v
@@ -83,7 +83,7 @@ Section ref.
     iIntros (α1 α2 Hα ty1 ty2 Hty q) "HL".
     iDestruct (Hty with "HL") as "#Hty". iDestruct (Hα with "HL") as "#Hα".
     iIntros "!# #HE". iDestruct ("Hα" with "HE") as "Hα1α2".
-    iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iAlways].
+    iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iModIntro].
     - done.
     - iIntros (tid [|[[]|][|[[]|][]]]) "H"=>//=.
       iDestruct "H" as (ν q' γ β ty') "(#Hshr & #H⊑ & #Hinv & Htok & Hown)".
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 25dc3ea207b4feaea2ec2142c4e23d2abeabf649..172ae8ee239a524eba75820022e31715c58a466a 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -317,8 +317,8 @@ Section ref_functions.
     iDestruct ("Hclose3" with "Hαν") as "[Hα Hν]".
     iMod ("Hclose2" with "Hϝ HL") as "HL".
     wp_rec. iDestruct "Hr" as "[Hr Hr†]".
-    iDestruct "Hr" as (?) "[Hr H]". iDestruct "H" as (vl1 ? ->) "[#Hr1' H]".
-    iDestruct "H" as (vl2 ? ->) "[#Hr2' ->]".
+    iDestruct "Hr" as (?) "[Hr H]". iDestruct "H" as (vl1 vl1' ->) "[#Hr1' H]".
+    iDestruct "H" as (vl2 vl2' ->) "[#Hr2' ->]".
     destruct vl1 as [|[[|lr1|]|] []], vl2 as [|[[|lr2|]|] []]=>//=.
     rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
     iDestruct "Hr" as "[Hr1 Hr2]". wp_read. wp_let. wp_op. wp_read. wp_let.
@@ -330,15 +330,15 @@ Section ref_functions.
     iMod (na_bor_acc with "LFT Hinv Hβ Hna") as "(INV & Hna & Hclosena)"; [done..|].
     wp_seq. wp_op. wp_read.
     iDestruct (refcell_inv_reading_inv with "INV Hγ")
-      as (q' n) "(H↦lrc & _ & [H● H◯] & H† & Hq' & Hshr')".
-    iDestruct "Hq'" as (q'') "(Hq'q'' & Hν1 & Hν2)".
-    iDestruct "Hq'q''" as %Hq'q''. iMod (own_update with "H●") as "[H● ?]".
+      as (q1 n) "(H↦lrc & _ & [H● H◯] & H† & Hq1 & Hshr')".
+    iDestruct "Hq1" as (q2) "(Hq1q2 & Hν1 & Hν2)".
+    iDestruct "Hq1q2" as %Hq1q2. iMod (own_update with "H●") as "[H● ?]".
     { apply auth_update_alloc,
-         (op_local_update_discrete _ _ (reading_stR (q''/2)%Qp ν))=>-[Hagv _].
+         (op_local_update_discrete _ _ (reading_stR (q2/2)%Qp ν))=>-[Hagv _].
       split; [split|done].
       - by rewrite /= agree_idemp.
-      - apply frac_valid'. rewrite -Hq'q'' comm -{2}(Qp_div_2 q'').
-        apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q''/2)%Qp).
+      - apply frac_valid'. rewrite -Hq1q2 comm -{2}(Qp_div_2 q2).
+        apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q2/2)%Qp).
         apply Qcplus_le_mono_r, Qp_ge_0. }
     wp_let. wp_read. wp_let. wp_op. wp_write.
     wp_apply (wp_delete _ _ _ [_; _] with "[Href↦1 Href↦2 Href†]")=>//.
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index d58a9b07a3a0004fcb2ce59199c93d19581293cf..dd212d5d358ec5e88d5d54007961ec4dce8c2a73 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -81,7 +81,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.
-      iNext; iAlways; iSplit; iIntros "H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl;
+      iNext; iModIntro; 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 [[[[ν rw] q' ] n]|]; try done;
@@ -192,7 +192,7 @@ Section refcell.
     - iPureIntro. simpl. congruence.
     - destruct vl as [|[[]|]]=>//=. by iApply "Hown".
     - simpl. iDestruct "H" as (a γ) "[Ha H]". iExists a, γ. iFrame.
-      iApply na_bor_iff; last done. iNext; iAlways; iSplit; iIntros "H".
+      iApply na_bor_iff; last done. iNext; iModIntro; iSplit; iIntros "H".
       by iApply "Hty1ty2". by iApply "Hty2ty1".
   Qed.
   Lemma refcell_mono' E L ty1 ty2 :
diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v
index 0ba4b8eb2f27a8c33ca95e2d01eb163d3001ad26..4c92b64da7ad6d1fc17985c69fc743c0e884a5a4 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -88,14 +88,14 @@ Section refmut.
     intros α1 α2 Hα ty1 ty2. rewrite eqtype_unfold=>Hty. iIntros (q) "HL".
     iDestruct (Hty with "HL") as "#Hty". iDestruct (Hα with "HL") as "#Hα".
     iIntros "!# #HE". iDestruct ("Hα" with "HE") as "Hα1α2".
-    iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iAlways].
+    iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iModIntro].
     - done.
     - iIntros (tid [|[[]|][|[[]|][]]]) "H"=>//=.
       iDestruct "H" as (ν γ q' β ty') "(Hb & #H⊑ & #Hinv & Hν & Hown)".
       iExists ν, γ, q', β, ty'. iFrame "∗#". iSplit.
       + iApply bor_shorten; last iApply bor_iff; last done.
         * iApply lft_intersect_mono; first done. iApply lft_incl_refl.
-        * iNext; iAlways; iSplit; iIntros "H"; iDestruct "H" as (vl) "[??]";
+        * iNext; iModIntro; 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 621b03cdf76148c2ce4e6e37d1d331dc636a2210..46f484d616f5c47c1b5b1055de419247719d728b 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -287,8 +287,8 @@ Section refmut_functions.
     iDestruct ("Hclose3" with "Hαν") as "[Hα Hν]".
     iMod ("Hclose2" with "Hϝ HL") as "HL".
     wp_rec. iDestruct "Hr" as "[Hr Hr†]".
-    iDestruct "Hr" as (?) "[Hr H]". iDestruct "H" as (vl1 ? ->) "[Hr1' H]".
-    iDestruct "H" as (vl2 ? ->) "[Hr2' ->]".
+    iDestruct "Hr" as (?) "[Hr H]". iDestruct "H" as (vl1 vl1' ->) "[Hr1' H]".
+    iDestruct "H" as (vl2 vl2' ->) "[Hr2' ->]".
     destruct vl1 as [|[[|lr1|]|] []], vl2 as [|[[|lr2|]|] []]=>//=.
     rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
     iDestruct "Hr" as "[Hr1 Hr2]". wp_read. wp_let. wp_op. wp_read. wp_let.
@@ -304,14 +304,14 @@ Section refmut_functions.
     destruct st as [[[[??]?]?]|]; last by destruct Hst as [[?|] Hst]; inversion Hst.
     move:Hst=>/Some_pair_included [/Some_pair_included_total_1
               [/to_agree_included /(leibniz_equiv _ _) [= <- <-] _] _].
-    iDestruct "Hst" as "(H† & Hq & _)". iDestruct "Hq" as (q' Hqq') "[Hν1 Hν2]".
+    iDestruct "Hst" as "(H† & Hq & _)". iDestruct "Hq" as (q1 Hqq1) "[Hν1 Hν2]".
     iMod (own_update with "H●") as "[H● ?]".
     { apply auth_update_alloc,
-         (op_local_update_discrete _ _ (writing_stR (q'/2)%Qp ν))=>-[Hagv _].
+         (op_local_update_discrete _ _ (writing_stR (q1/2)%Qp ν))=>-[Hagv _].
       split; [split|done].
       - by rewrite /= agree_idemp.
-      - apply frac_valid'. rewrite -Hqq' comm -{2}(Qp_div_2 q').
-        apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q'/2)%Qp).
+      - apply frac_valid'. rewrite -Hqq1 comm -{2}(Qp_div_2 q1).
+        apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q1/2)%Qp).
         apply Qcplus_le_mono_r, Qp_ge_0. }
     wp_let. wp_read. wp_let. wp_op. wp_write.
     wp_apply (wp_delete _ _ _ [_; _] with "[Hrefmut↦1 Hrefmut↦2 Hrefmut†]")=>//.
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index c57eea56a2405108100b9391bb33c2da746d9264..75a24847e59c0d5d16f8d99106e261f551c42679 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -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.
-      iNext; iAlways; iSplit; iIntros "H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl;
+      iNext; iModIntro; 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;
@@ -178,7 +178,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. iNext; iAlways; iSplit; iIntros "H".
+      iApply at_bor_iff; last done. iNext; iModIntro; iSplit; iIntros "H".
       by iApply "Hty1ty2". by iApply "Hty2ty1".
   Qed.
   Lemma rwlock_mono' E L ty1 ty2 :
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 7b468ca82d1144a7543fe8755d6577e5980f1a46..8cc6561c4c25560bb3b43a58ef394cadcf54d272 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -83,7 +83,7 @@ Section rwlockreadguard.
     iDestruct (rwlock_inv_proper with "HL") as "#Hty1ty2"; first done.
     iDestruct (rwlock_inv_proper with "HL") as "#Hty2ty1"; first by symmetry.
     iIntros "!# #HE". iDestruct ("Hα" with "HE") as "Hα1α2".
-    iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iAlways].
+    iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iModIntro].
     - done.
     - iIntros (tid [|[[]|][]]) "H"; try done.
       iDestruct "H" as (ν q' γ β) "(#Hshr & #H⊑ & #Hinv & Htok & Hown)".
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index aabe30e73f7ad86a30ec3900f034bfd94817e528..7b8576d5ca62f9a0bae082df5be29d4d375183a6 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -81,13 +81,13 @@ Section rwlockwriteguard.
     iDestruct (rwlock_inv_proper with "HL") as "#Hty1ty2"; first done.
     iDestruct (rwlock_inv_proper with "HL") as "#Hty2ty1"; first by symmetry.
     iIntros "!# #HE". iDestruct ("Hα" with "HE") as "Hα1α2".
-    iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iAlways].
+    iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iModIntro].
     - done.
     - iIntros (tid [|[[]|][]]) "H"; try done.
       iDestruct "H" as (γ β) "(Hb & #H⊑ & #Hinv & Hown)".
       iExists γ, β. iFrame "∗#". iSplit; last iSplit.
       + iApply bor_iff; last done.
-        iNext; iAlways; iSplit; iIntros "H"; iDestruct "H" as (vl) "[??]";
+        iNext; iModIntro; iSplit; iIntros "H"; iDestruct "H" as (vl) "[??]";
         iExists vl; iFrame; by iApply "Ho".
       + by iApply lft_incl_trans.
       + iApply at_bor_iff; try done.
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index 53a3a252cd97e388f9c503ceef12f72b0aaef129..f6caa8ea7339a49895aabe12a0fa3682ec9360f3 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -30,7 +30,7 @@ Section join_handle.
   Lemma join_handle_subtype ty1 ty2 :
     ▷ type_incl ty1 ty2 -∗ type_incl (join_handle ty1) (join_handle ty2).
   Proof.
-    iIntros "#Hincl". iSplit; first done. iSplit; iAlways.
+    iIntros "#Hincl". iSplit; first done. iSplit; iModIntro.
     - iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
       simpl. iApply (join_handle_impl with "[] Hvl"). clear tid.
       iIntros "!# * Hown" (tid).
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 22cfa025e8a2aaac160e041714fdd7e8a3353531..2deec3a41d025ae81a95b0c1260e84c91dc5ad92 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -93,7 +93,7 @@ Section own.
   Lemma own_type_incl n m ty1 ty2 :
     ▷ ⌜n = m⌝ -∗ ▷ type_incl ty1 ty2 -∗ type_incl (own_ptr n ty1) (own_ptr m ty2).
   Proof.
-    iIntros "#Heq (#Hsz & #Ho & #Hs)". iSplit; first done. iSplit; iAlways.
+    iIntros "#Heq (#Hsz & #Ho & #Hs)". iSplit; first done. iSplit; iModIntro.
     - iIntros (?[|[[| |]|][]]) "H"; try done. simpl.
       iDestruct "H" as "[Hmt H†]". iNext. iDestruct ("Hsz") as %<-.
       iDestruct "Heq" as %->. iFrame. iApply (heap_mapsto_pred_wand with "Hmt").
@@ -140,7 +140,7 @@ Section own.
     Sync ty → Sync (own_ptr n ty).
   Proof.
     iIntros (Hsync κ tid1 tid2 l) "H". iDestruct "H" as (l') "[Hm #Hshr]".
-    iExists _. iFrame "Hm". iAlways. iIntros (F q) "% Htok".
+    iExists _. iFrame "Hm". iModIntro. iIntros (F q) "% Htok".
     iMod ("Hshr" with "[] Htok") as "Hfin"; first done. iModIntro. iNext.
     iMod "Hfin" as "{Hshr} [Hshr $]". by iApply Hsync.
   Qed.
@@ -240,7 +240,7 @@ Section typing.
   Lemma read_own_move E L ty n :
     ⊢ typed_read E L (own_ptr n ty) ty (own_ptr n $ uninit ty.(ty_size)).
   Proof.
-    rewrite typed_read_eq. iAlways.
+    rewrite typed_read_eq. iModIntro.
     iIntros ([[]|] tid F qL ?) "_ _ $ $ Hown"; try done.
     iDestruct "Hown" as "[H↦ H†]". iDestruct "H↦" as (vl) "[>H↦ Hown]".
     iDestruct (ty_size_eq with "Hown") as "#>%".
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 42bed577d8fb04a885e74b1df51eb67a1d6024dd..c0e28c9bcb6e4a3f1016e3195a0f336baf888e81 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -94,7 +94,7 @@ Section product.
     iClear "∗". iIntros "!# #HE".
     iDestruct ("H1" with "HE") as "#(% & #Ho1 & #Hs1)". clear H1.
     iDestruct ("H2" with "HE") as "#(% & #Ho2 & #Hs2)". clear H2.
-    iSplit; first by (iPureIntro; simpl; f_equal). iSplit; iAlways.
+    iSplit; first by (iPureIntro; simpl; f_equal). iSplit; iModIntro.
     - iIntros (??) "H". iDestruct "H" as (vl1 vl2) "(% & Hown1 & Hown2)".
       iExists _, _. iSplit. done. iSplitL "Hown1".
       + by iApply "Ho1".
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 2e69050734f921dc6cb0e941147a1701b59fb994..2d8c32adc4c349465762cace5e04820d976c345c 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -130,7 +130,7 @@ Section sum.
     { iInduction Htyl as [|???? Hsub] "IH".
       { iClear "∗". iIntros "!# _". done. }
       iDestruct (Hsub with "HL") as "#Hsub". iDestruct ("IH" with "HL") as "{IH} #IH".
-      iAlways. iIntros "#HE". iDestruct ("Hsub" with "HE") as "(% & _ & _)".
+      iModIntro. iIntros "#HE". iDestruct ("Hsub" with "HE") as "(% & _ & _)".
       iDestruct ("IH" with "HE") as %IH. iPureIntro. simpl. inversion_clear IH. by f_equal. }
     iDestruct (subtype_Forall2_llctx with "HL") as "#Htyl"; first done.
     iClear "HL". iIntros "!# #HE".
@@ -146,11 +146,11 @@ Section sum.
         rewrite (nth_lookup_Some tyl2 _ _ ty2) //. }
     clear -Hleq. iClear "∗". iSplit; last iSplit.
     - simpl. by rewrite Hleq.
-    - iAlways. iIntros (tid vl) "H". iDestruct "H" as (i vl' vl'') "(% & % & Hown)".
+    - iModIntro. iIntros (tid vl) "H". iDestruct "H" as (i vl' vl'') "(% & % & Hown)".
       iExists i, vl', vl''. iSplit; first done.
       iSplit; first by rewrite -Hleq.
       iDestruct ("Hty" $! i) as "(_ & #Htyi & _)". by iApply "Htyi".
-    - iAlways. iIntros (κ tid l) "H". iDestruct "H" as (i) "(Hmt & Hshr)".
+    - iModIntro. iIntros (κ tid l) "H". iDestruct "H" as (i) "(Hmt & Hshr)".
       iExists i. iSplitR "Hshr".
       + rewrite /is_pad -Hleq. iDestruct ("Hty" $! i) as "(Hlen & _)".
         iDestruct "Hlen" as %<-. done.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 9da92246772fed47e3ee3bf2f9fdc9f7cb25f1be..905b05c4d1e21c9495c7e1feb38694402d596990 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -548,14 +548,14 @@ Section subtyping.
   Global Instance type_incl_persistent ty1 ty2 : Persistent (type_incl ty1 ty2) := _.
 
   Lemma type_incl_refl ty : ⊢ type_incl ty ty.
-  Proof. iSplit; first done. iSplit; iAlways; iIntros; done. Qed.
+  Proof. iSplit; first done. iSplit; iModIntro; iIntros; done. Qed.
 
   Lemma type_incl_trans ty1 ty2 ty3 :
     type_incl ty1 ty2 -∗ type_incl ty2 ty3 -∗ type_incl ty1 ty3.
   Proof.
     iIntros "(% & #Ho12 & #Hs12) (% & #Ho23 & #Hs23)".
     iSplit; first (iPureIntro; etrans; done).
-    iSplit; iAlways; iIntros.
+    iSplit; iModIntro; iIntros.
     - iApply "Ho23". iApply "Ho12". done.
     - iApply "Hs23". iApply "Hs12". done.
   Qed.
@@ -643,7 +643,7 @@ Section subtyping.
     □ (∀ tid vl, st1.(st_own) tid vl -∗ st2.(st_own) tid vl) -∗
     type_incl st1 st2.
   Proof.
-    iIntros "#Hst". iSplit; first done. iSplit; iAlways.
+    iIntros "#Hst". iSplit; first done. iSplit; iModIntro.
     - iIntros. iApply "Hst"; done.
     - iIntros (???). iDestruct 1 as (vl) "[Hf Hown]". iExists vl. iFrame "Hf".
       by iApply "Hst".
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index d2c80811f9e57bb553f40c704235b3b888f170d6..95d7aaf4182cd90ff1012869d34eae6461d586d9 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -51,10 +51,10 @@ Section uniq_bor.
     iDestruct (Hty with "HL") as "#Hty". iDestruct (Hκ with "HL") as "#Hκ".
     iIntros "!# #HE". iSplit; first done.
     iDestruct ("Hty" with "HE") as "(_ & #Ho & #Hs)"; [done..|clear Hty].
-    iSpecialize ("Hκ" with "HE"). iSplit; iAlways.
+    iSpecialize ("Hκ" with "HE"). iSplit; iModIntro.
     - iIntros (? [|[[]|][]]) "H"; try done.
       iApply (bor_shorten with "Hκ"). iApply bor_iff; last done.
-      iNext. iAlways. iSplit; iIntros "H"; iDestruct "H" as (vl) "[??]";
+      iNext. iModIntro. 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. }
@@ -81,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 bi.equiv_iff.
+    iApply bor_iff; last done. iNext. iModIntro. iApply bi.equiv_iff.
     do 3 f_equiv. iSplit; iIntros "."; by iApply Hsend.
   Qed.
 
@@ -89,7 +89,7 @@ Section uniq_bor.
     Sync ty → Sync (uniq_bor κ ty).
   Proof.
     iIntros (Hsync κ' tid1 tid2 l) "H". iDestruct "H" as (l') "[Hm #Hshr]".
-    iExists l'. iFrame "Hm". iAlways. iIntros (F q) "% Htok".
+    iExists l'. iFrame "Hm". iModIntro. iIntros (F q) "% Htok".
     iMod ("Hshr" with "[] Htok") as "Hfin"; first done. iClear "Hshr".
     iModIntro. iNext. iMod "Hfin" as "[Hshr $]". iApply Hsync. done.
   Qed.