diff --git a/opam.pins b/opam.pins
index 202664902296013ad5d1896abfca2d49917d8de5..47804d3c16e251ff2fa80955b3d65167e7471625 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 1e241cca15302ae89d41f14251c2dafbd7efebb6
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 26e93ebf7d4cfcd4c1c278c2e57ad0ae12a97ab6
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 4bc0cada0183315cbdba5051eab0d7599291bdb0..4d075647a35339279cd78c07daba29219d4ff5b9 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -83,7 +83,7 @@ Section borrow.
     wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
     iDestruct "Hown" as (l') "#[H↦b #Hown]".
     iMod (frac_bor_acc with "LFT H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
-    iApply (wp_fupd_step _ (_∖_) with "[Hown Htok2]"); try done.
+    iApply (wp_step_fupd _ (_∖_) with "[Hown Htok2]"); try done.
     - iApply ("Hown" with "[%] Htok2"). set_solver+.
     - iApply wp_fupd. wp_read. iIntros "!>[#Hshr Htok2]".
       iMod ("Hclose'" with "[H↦]") as "Htok1"; first by auto.
@@ -115,7 +115,7 @@ Section borrow.
       try by iMod (bor_persistent_tok with "LFT Hbor Htok") as "[>[] _]".
     iMod (bor_acc with "LFT H↦ Htok") as "[>H↦ Hclose']". done.
     rewrite heap_mapsto_vec_singleton.
-    iApply (wp_fupd_step  _ (⊤∖↑lftN) with "[Hbor]"); try done.
+    iApply (wp_step_fupd  _ (⊤∖↑lftN) with "[Hbor]"); try done.
       by iApply (bor_unnest with "LFT Hbor").
     iApply wp_fupd. wp_read. iIntros "!> Hbor".
     iMod ("Hclose'" with "[H↦]") as "[H↦ Htok]"; first by auto.
@@ -147,7 +147,7 @@ Section borrow.
     iAssert (κ ⊑ κ' ⊓ κ)%I as "#Hincl'".
     { iApply (lft_incl_glb with "Hincl []"). iApply lft_incl_refl. }
     iMod (lft_incl_acc with "Hincl' Htok2") as (q2) "[Htok2 Hclose'']". solve_ndisj.
-    iApply (wp_fupd_step _ (_∖_) with "[Hown Htok2]"); try done.
+    iApply (wp_step_fupd _ (_∖_) with "[Hown Htok2]"); try done.
     - iApply ("Hown" with "[%] Htok2"). set_solver+.
     - iApply wp_fupd. wp_read. iIntros "!>[#Hshr Htok2]".
       iMod ("Hclose''" with "Htok2") as "Htok2".
diff --git a/theories/typing/lib/option.v b/theories/typing/lib/option.v
index 720310ac321e1ba174420d7ed2b931f5cf0b8495..b8182aa739eb8fe91e953b5b67822f7738f8f6e1 100644
--- a/theories/typing/lib/option.v
+++ b/theories/typing/lib/option.v
@@ -29,7 +29,7 @@ Section option.
       iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
       iApply type_case_uniq; [solve_typing..|].
         constructor; last constructor; last constructor; left.
-      + iApply (type_sum_assign_unit [unit; &uniq{α}τ]%T); [solve_typing..|].
+      + iApply (type_sum_unit [unit; &uniq{α}τ]%T); [solve_typing..|].
         iApply (type_jump [_]); solve_typing.
       + iApply (type_sum_assign [unit; &uniq{α}τ]%T); [solve_typing..|].
         iApply (type_jump [_]); solve_typing.
diff --git a/theories/typing/lib/rc.v b/theories/typing/lib/rc.v
index c83a2b99ae6b0515497d4ebbbccc179ba734afa2..84c34419497ca43632a86ac84e6b120f8941f1ca 100644
--- a/theories/typing/lib/rc.v
+++ b/theories/typing/lib/rc.v
@@ -29,7 +29,10 @@ Section rc.
       | Some (q, c) => ∃ q',
        l ↦ #(Zpos c) ∗ †{1%Qp}l…(S ty.(ty_size)) ∗
          ⌜(q + q')%Qp = 1%Qp⌝ ∗ q'.[ν] ∗
-         (1.[ν] ={↑lftN,∅}▷=∗ ▷ shift_loc l 1 ↦∗: ty.(ty_own) tid)
+         (* We keep this view shift decomposed because we store the persistent part
+            also in ty_own, to make it available with one step less. *)
+         ([†ν] ={↑lftN}=∗ ▷ shift_loc l 1 ↦∗: ty.(ty_own) tid) ∗
+         □ (1.[ν] ={↑lftN,∅}▷=∗ [†ν])
       | None => True
       end)%I.
 
@@ -40,8 +43,9 @@ Section rc.
          | [ #(LitLoc l) ] =>
            (l ↦ #1 ∗ †{1%Qp}l…(S ty.(ty_size)) ∗ ▷ shift_loc l 1 ↦∗: ty.(ty_own) tid) ∨
            (∃ γ ν q, na_inv tid rc_invN (rc_inv tid ν γ l ty) ∗
-                     own γ (◯ Some (q, 1%positive)) ∗ q.[ν] ∗
-                     ty.(ty_shr) ν tid (shift_loc l 1))
+                     own γ (◯ Some (q, 1%positive)) ∗
+                     ty.(ty_shr) ν tid (shift_loc l 1) ∗
+                     q.[ν] ∗ □ (1.[ν] ={↑lftN,∅}▷=∗ [†ν]))
          | _ => False end;
        ty_shr κ tid l :=
          ∃ (l' : loc), &frac{κ} (λ q, l ↦∗{q} [ #l']) ∗
@@ -82,13 +86,12 @@ Section rc.
         iMod (own_alloc (● Some ((1/2)%Qp, 1%positive) ⋅ ◯ Some ((1/2)%Qp, 1%positive))) as (γ) "[Ha Hf]".
         { apply auth_valid_discrete_2. done. }
         iMod (na_inv_alloc tid _ _ (rc_inv tid ν γ l' ty) with "[Ha Hν2 Hl' H† HPend]").
-        { rewrite /rc_inv. iExists (Some (_, _)). iFrame. iExists _. iFrame.
-          iNext. iSplit; first by rewrite Qp_div_2. iIntros "Hν".
-          iMod ("Hν†" with "Hν") as "Hfin". iModIntro. iNext. iMod "Hfin".
-          iMod ("HPend" with "Hfin"). done. }
+        { rewrite /rc_inv. iExists (Some (_, _)). iFrame. iExists _. iFrame "#∗".
+          (* FIXME: iFrame fails to frame Hν†. *)
+          iNext. iSplit; last by iAlways. by rewrite Qp_div_2. }
         iMod (ty_share with "LFT HP Hν1") as "[??]"; first solve_ndisj.
         iExists _, _, _. iFrame. done. }
-      iDestruct "HX" as (γ ν q') "(#Hinv & Hrc & Htok & #Hshr)".
+      iDestruct "HX" as (γ ν q') "(#Hinv & Hrc & #Hshr & Htok & #Hν†)".
       iMod ("Hclose2" with "[] [Hrc Htok]") as "[HX Htok]".
       { iNext. iIntros "HX". iModIntro. iNext.
         iRight. iExists γ, ν, q'. iExact "HX". }
@@ -97,6 +100,7 @@ Section rc.
       { iExists _, _, _. iFrame "Hinv".
         iMod (bor_sep with "LFT HX") as "[_ HX]"; first solve_ndisj.
         iMod (bor_sep with "LFT HX") as "[Hrc HX]"; first solve_ndisj.
+        iMod (bor_sep with "LFT HX") as "[_ HX]"; first solve_ndisj.
         iMod (bor_sep with "LFT HX") as "[Hlft _]"; first solve_ndisj.
         iDestruct (frac_bor_lft_incl with "LFT >[Hlft]") as "#Hlft".
         { iApply (bor_fracture with "LFT"); first solve_ndisj. by rewrite Qp_mult_1_r. }
@@ -197,7 +201,7 @@ Section code.
     (* All right, we are done preparing our context. Let's get going. *)
     rewrite {1}/elctx_interp big_sepL_singleton.
     iDestruct "HE" as "[Hα1 Hα2]". wp_bind (!_)%E.
-    iSpecialize ("Hshr" with "[] Hα1"); last iApply (wp_fupd_step with "Hshr"); [done..|].
+    iSpecialize ("Hshr" with "[] Hα1"); last iApply (wp_step_fupd with "Hshr"); [done..|].
     iMod (frac_bor_acc with "LFT Hlrc Hα2") as (q') "[Hlrc↦ Hclose]"; first solve_ndisj.
     rewrite heap_mapsto_vec_singleton. iApply wp_fupd. wp_read.
     iMod ("Hclose" with "[$Hlrc↦]") as "Hα2". iIntros "!> [Hα1 Hproto]".
@@ -208,7 +212,7 @@ Section code.
     iMod (na_bor_acc with "LFT Hrctokb Hα1 Hna") as "(>Hrctok & Hna & Hclose2)"; [solve_ndisj..|].
     iDestruct "Hrcproto" as (st) "[>Hrc● Hrcst]".
     iDestruct (own_valid_2 with "Hrc● Hrctok") as %[[Hval|[_ [[qa c] [_ [-> _]]]]]%option_included _]%auth_valid_discrete_2; first done. (* Oh my, what a pattern... *)
-    iDestruct "Hrcst" as (qb) "(>Hl' & >Hl'† & >% & Hνtok & Hν†)".
+    iDestruct "Hrcst" as (qb) "(>Hl' & >Hl'† & >% & Hνtok & Hν† & #Hνend)".
     wp_read. wp_let. wp_op. rewrite shift_loc_0. wp_op. wp_write. wp_write.
     (* And closing it again. *)
     iMod (own_update with "Hrc●") as "[Hrc● Hrctok2]".
@@ -221,7 +225,9 @@ Section code.
     iMod ("Hclose2" with "[$Hrctok] Hna") as "[Hα1 Hna]".
     iMod ("Hclose1" with "[Hrc● Hl' Hl'† Hνtok2 Hν† $Hna]") as "Hna".
     { iExists _. iFrame "Hrc●". iExists _. rewrite Z.add_comm. iFrame.
-      iNext. iPureIntro. rewrite [_ â‹… _]comm frac_op' -assoc Qp_div_2. done. }
+      (* FIXME: iFrame fails to frame Hνend. *)
+      iNext. iSplit; last by iAlways.
+      iPureIntro. rewrite [_ â‹… _]comm frac_op' -assoc Qp_div_2. done. }
     (* Finish up the proof. *)
     iApply (type_type _ _ _ [ x ◁ box (&shr{α} rc ty); #lrc2 ◁ box (rc ty)]%TC
         with "[] LFT Hna [Hα1 Hα2] HL Hk [-]"); last first.
@@ -249,17 +255,17 @@ Section code.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
     iIntros (tid qE) "#LFT Hna HE HL Hk".
     rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
-    iIntros "[Hrcx [Hrc' Hx]]".
+    iIntros "[Hrcx [Hrc' Hx]]". rewrite [[rcx]]lock.
     destruct x as [[|x|]|]; try done.
     (* FIXME why is x printed in the code as "LitV x", not "#x"? *)
     iDestruct "Hx" as "[Hx Hx†]". iDestruct "Hx" as (vl) "[>Hx >SZ]".
     rewrite uninit_own. destruct vl as [|]; iDestruct "SZ" as %[=].
     destruct vl as [|]; last done. rewrite heap_mapsto_vec_singleton.
-    rewrite [[rcx]]lock. destruct rc' as [[|rc'|]|]; try done. simpl.
+    destruct rc' as [[|rc'|]|]; try done. simpl.
     iDestruct "Hrc'" as (l') "[#Hrc' #Hdelay]".
     (* All right, we are done preparing our context. Let's get going. *)
     rewrite {1}/elctx_interp big_sepL_singleton. iDestruct "HE" as "[Hα1 Hα2]". wp_bind (!_)%E.
-    iSpecialize ("Hdelay" with "[] Hα1"); last iApply (wp_fupd_step with "Hdelay"); [done..|].
+    iSpecialize ("Hdelay" with "[] Hα1"); last iApply (wp_step_fupd with "Hdelay"); [done..|].
     iMod (frac_bor_acc with "LFT Hrc' Hα2") as (q') "[Hrc'↦ Hclose]"; first solve_ndisj.
     rewrite heap_mapsto_vec_singleton. iApply wp_fupd. wp_read.
     iMod ("Hclose" with "[$Hrc'↦]") as "Hα2". iIntros "!> [Hα1 Hproto]".
@@ -279,22 +285,127 @@ Section code.
   Definition rc_drop ty : val :=
     funrec: <> ["rc"] :=
       let: "x" := new [ #(option ty).(ty_size) ] in
-      let: "rc'" := !"rc" in
-      let: "count" := (!"rc'" +â‚— #0) in
+      (let: "rc'" := !"rc" in
+      let: "count" := !("rc'" +â‚— #0) in
       "rc'" +â‚— #0 <- "count" - #1;;
       if: "count" = #1 then
         (* Return content, delete Rc heap allocation. *)
         "x" <-{ty.(ty_size),Σ 1} !("rc'" +ₗ #1);;
         delete [ #(S ty.(ty_size)); "rc'" ];;
-        "k" ["x"]
+        "k" []
       else
         "x" <-{Σ 0} ();;
-        "k" ["x"]
-      cont: "k" ["x"] :=
-        delete [ #1; "rc"];; return: ["x"].
+        "k" []
+      cont: "k" [] :=
+        delete [ #1; "rc"];; return: ["x"]).
+
+  Lemma rc_check_unique ty F tid (l : loc) :
+    ↑rc_invN ⊆ F →
+    {{{ na_own tid F ∗ ty_own (rc ty) tid [ #l ] }}}
+    !#l
+    {{{ c, RET #(Zpos c); l ↦ #(Zpos c) ∗
+        ((⌜c = 1%positive⌝ ∗ †{1%Qp}l…(S ty.(ty_size)) ∗ na_own tid F ∗ ▷ shift_loc l 1 ↦∗: ty.(ty_own) tid) ∨
+         (⌜(1 < c)%positive⌝ ∗ na_own tid (F ∖ ↑rc_invN) ∗
+          ∃ γ ν q q', na_inv tid rc_invN (rc_inv tid ν γ l ty) ∗
+            own γ (◯ Some (q, 1%positive)) ∗ own γ (● Some ((q + q')%Qp, c)) ∗
+            q.[ν] ∗ ty.(ty_shr) ν tid (shift_loc l 1) ∗
+            (∀ c' q'', own γ (● Some (q'', c')) ∗ l ↦ #(Zpos c') ∗
+                       (⌜(q + q')%Qp = q''⌝ ∨ ∃ qg, ⌜(q + q' = qg + q'')%Qp⌝ ∗ qg.[ν]) ∗ na_own tid (F ∖ ↑rc_invN) ={⊤}=∗ 
+                       na_own tid F) )
+        ) }}}.
+  Proof.
+    iIntros (? Φ) "[Hna [(Hl & H† & Hown)|Hown]] HΦ".
+    - wp_read. iApply "HΦ". auto with iFrame.
+    - iDestruct "Hown" as (γ ν q) "(#Hinv & Htok & #Hshr & Hν1 & #Hνend)".
+      iMod (na_inv_open with "Hinv Hna") as "(Hproto & Hna & Hclose)"; [solve_ndisj..|].
+      iDestruct "Hproto" as (st) "[>Hst Hproto]".
+      iDestruct (own_valid_2 with "Hst Htok") as %[[Hval|[? [[qa c] [[=<-] [-> Hst]]]]]%option_included _]%auth_valid_discrete_2; first done. (* Oh my, what a pattern... *)
+      iDestruct "Hproto" as (q') "(>Hl & H† & >% & >Hν2 & Hν† & _)". iApply wp_fupd.
+      destruct (decide (c ≤ 1)%positive) as [Hle|Hnle].
+      + (* Tear down the protocol. *)
+        assert (c = 1%positive) as ->.
+        { apply Pos.le_antisym; first done. exact: Pos.le_1_l. } clear Hle.
+        destruct Hst as [[??]|[_ Hle%pos_included]%prod_included]; last first.
+        { exfalso. eapply Pos.nlt_1_r. done. }
+        setoid_subst. iMod (own_update_2 with "Hst Htok") as "Hst".
+        { apply auth_update_dealloc. rewrite -(right_id None _ (Some _)).
+          apply cancel_local_update_empty, _. }
+        iMod ("Hclose" with "[$Hna Hst]") as "Hna".
+        { iExists None. auto. }
+        iSpecialize ("Hνend" with "[Hν1 Hν2]").
+        { rewrite -H0. iFrame. }
+        iApply wp_mask_mono; last iApply (wp_step_fupd with "Hνend"); [done..|try solve_ndisj|].
+        { (* FIXME: solve_ndisj should solve this... *) set_solver+. }
+        wp_read. iIntros "#Hν". iMod ("Hν†" with "Hν") as "Hown". iModIntro.
+        iApply "HΦ". iFrame. iLeft. auto with iFrame.
+      + destruct Hst as [[??%leibniz_equiv]|[[q'' Hqa%leibniz_equiv] ?%pos_included]%prod_included].
+        { exfalso. simpl in *. subst c. apply Hnle. done. }
+        simpl in *. subst qa. wp_read. iApply "HΦ". iFrame. iRight. iModIntro. iSplit.
+        { iPureIntro. apply Pos.lt_nle. done. }
+        iFrame "Hna". iExists _, _, q, q''. iFrame "#∗%".
+        iIntros (c' qx) "(Hst & Hl & Hq'' & Hna)". iApply "Hclose". iFrame "Hna".
+        iExists _. iFrame "Hst". iDestruct "Hq''" as "[%|Hq'']".
+        * iExists _. subst qx. iFrame "∗%". by iIntros "!> !#".
+        * iDestruct "Hq''" as (qg) "[% Hν']". iExists _. 
+          iCombine "Hν2 Hν'" as "Hν". iFrame. iNext. iSplit; last by iAlways.
+          iPureIntro. rewrite [(q' + _)%Qp]comm_L assoc [(qx + _)%Qp]comm_L -H1. done.
+  Qed.
 
   Lemma rc_drop_type ty :
     typed_val (rc_drop ty) (fn([]; rc ty) → option ty).
-  Proof. Abort.
+  Proof.
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (_ ret arg). inv_vec arg=>rcx. simpl_subst.
+    iApply type_new; [solve_typing..|]; iIntros (x); simpl_subst. rewrite (Nat2Z.id (option ty).(ty_size)).
+    iApply (type_cont [] [] (λ r, [rcx ◁ box (uninit 1); x ◁ box (option ty)])%TC) ; [solve_typing..| |]; last first.
+    { simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
+      iApply type_delete; [solve_typing..|].
+      iApply (type_jump [_]); solve_typing. }
+    iIntros (k). simpl_subst.
+    iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
+    iIntros (tid qE) "#LFT Hna HE HL Hk".
+    rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
+    iIntros "[Hrcx [Hrc' Hx]]".
+    destruct rc' as [[|rc'|]|]; try done. rewrite [[rcx]]lock [[x]]lock [[ #rc' ]]lock.
+    wp_op. rewrite shift_loc_0. rewrite -(lock [ #rc' ]).
+    wp_apply (rc_check_unique with "[$Hna $Hrc']"); first solve_ndisj.
+    iIntros (c) "(Hrc & Hc)". wp_let. wp_op. rewrite shift_loc_0.
+    rewrite {3}[Z.pos c]lock. wp_op.
+    iDestruct "Hc" as "[(% & Hrc† & Hna & Hown)|(% & Hna & Hproto)]".
+    - subst c. wp_write. wp_op=>[_|?]; last done. wp_if.
+      iApply (type_type _ _ _ [ x ◁ own_ptr (ty_size (option ty)) (uninit _);
+                                rcx ◁ box (uninit 1);
+                                #rc' +ₗ #1 ◁ own_ptr (S ty.(ty_size)) ty;
+                                #rc' +ₗ #0 ◁ own_ptr (S ty.(ty_size)) (uninit 1%nat)]%TC
+        with "[] LFT Hna HE HL Hk [-]"); last first.
+      { unlock. rewrite 3!tctx_interp_cons tctx_interp_singleton.
+        rewrite 2!tctx_hasty_val tctx_hasty_val' // tctx_hasty_val' //.
+        rewrite -freeable_sz_full_S -(freeable_sz_split _ 1%nat).
+        iDestruct "Hrc†" as "[Hrc†1 Hrc†2]". iFrame.
+        rewrite shift_loc_0. iFrame. iExists [_]. rewrite uninit_own heap_mapsto_vec_singleton.
+        auto with iFrame. }
+      iApply (type_sum_memcpy [unit;_]); [solve_typing..|].
+      iApply (type_delete (Π[uninit _; uninit _])); [solve_typing..|].
+      iApply (type_jump []); solve_typing.
+    - iDestruct "Hproto" as (γ ν q q') "(#Hinv & Hrctok & Hrc● & Hν & _ & Hclose)".
+      (* FIXME: linebreaks in "Hclose" do not look as expected. *)
+      wp_write. wp_op; intros Hc.
+      { exfalso. move:Hc. move/Zpos_eq_iff. intros ->. exact: Pos.lt_irrefl. }
+      wp_if. iMod ("Hclose" $! (c-1)%positive q' with ">[Hrc● Hrctok Hrc Hν $Hna]") as "Hna".
+      { unlock. iMod (own_update_2 with "Hrc● Hrctok") as "$".
+        { apply auth_update_dealloc. rewrite -{1}(Pplus_minus c 1%positive); last first.
+          { apply Pos.lt_gt. done. }
+          rewrite -pair_op Some_op. apply: cancel_local_update_empty.
+          (* For some reason, Coq's apply doesn't work here. whatever. *) }
+        rewrite Pos2Z.inj_sub //. iFrame "Hrc". iRight. iExists _.
+        auto with iFrame. }
+      iApply (type_type _ _ _ [ x ◁ own_ptr (ty_size (option ty)) (uninit _);
+                                rcx ◁ box (uninit 1)]%TC
+        with "[] LFT Hna HE HL Hk [-]"); last first.
+      { rewrite tctx_interp_cons tctx_interp_singleton.
+        rewrite !tctx_hasty_val. unlock. iFrame. }
+      iApply (type_sum_unit [unit;ty]); [solve_typing..|].
+      iApply (type_jump []); solve_typing.
+  Qed.
 
 End code.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 952f950eb315023aa8fb710a5a744f30671b767b..95e0224595068cbd4aafb5d9026bc3f419e1d446 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -190,7 +190,7 @@ Section ref_functions.
         iSplitR; first done. iExists (q+q'')%Qp. iFrame.
         by rewrite assoc (comm _ q0 q). }
     wp_bind Endlft. iApply (wp_mask_mono (↑lftN)); first done.
-    iApply (wp_fupd_step with "INV"); [set_solver..|]. wp_seq.
+    iApply (wp_step_fupd with "INV"); [set_solver..|]. wp_seq.
     iIntros "INV !>". wp_seq. iMod ("Hcloseβ" with "[$INV] Hna") as "[Hβ Hna]".
     iMod ("Hcloseα" with "Hβ") as "Hα".
     iApply (type_type _ _ _ [ #lx ◁ box (uninit 2)]%TC with "[] LFT Hna [Hα] HL Hk");
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index 93bb78de5f0458df6fdd87aa7638068a3cb2b1ec..f046c25d3c77829d71e20bbb0aca93c783da00fc 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -166,7 +166,7 @@ Section refcell_functions.
               with "[] LFT Hna >[Hclose Hβtok1 Hβtok2] HL Hk"); first last.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
-      iApply (type_sum_assign_unit [unit; ref α ty]); [solve_typing..|]; first last.
+      iApply (type_sum_unit [unit; ref α ty]); [solve_typing..|]; first last.
       simpl. iApply (type_jump [_]); solve_typing.
     - wp_op. wp_write. wp_apply wp_new; [done..|].
       iIntros (lref vl) "(EQ & H† & Hlref)". iDestruct "EQ" as %?%(inj Z.of_nat 2%nat).
@@ -300,7 +300,7 @@ Section refcell_functions.
               with "[] LFT Hna >[Hclose Hβtok] HL Hk"); first last.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
-      iApply (type_sum_assign_unit [unit; refmut α ty]); [solve_typing..|].
+      iApply (type_sum_unit [unit; refmut α ty]); [solve_typing..|].
       simpl. iApply (type_jump [_]); solve_typing.
   Qed.
 End refcell_functions.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 5602f7fbfc3ab0e13edda9ef770170afda91bb3f..72dd7335d5d45f9d23e775a2633062dcc3833747 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -34,7 +34,7 @@ Section refmut_functions.
     iMod (frac_bor_acc with "LFT Hfrac Hα1") as (qlx') "[H↦ Hcloseα1]". done.
     rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
     iDestruct (lft_intersect_acc with "Hβ Hα2") as (qβα) "[Hα2β Hcloseβα2]".
-    wp_bind (!(LitV lx'))%E. iApply (wp_fupd_step with "[Hα2β]");
+    wp_bind (!(LitV lx'))%E. iApply (wp_step_fupd with "[Hα2β]");
          [done| |by iApply ("Hshr" with "[] Hα2β")|]; first done.
     iMod "H↦" as "[H↦1 H↦2]". wp_read. iIntros "[#Hshr' Hα2β]!>". wp_let.
     iDestruct ("Hcloseβα2" with "Hα2β") as "[Hβ Hα2]".
@@ -89,7 +89,7 @@ Section refmut_functions.
     iDestruct (frac_bor_lft_incl _ _ 1 with "LFT H") as "#Hαν". iClear "H".
     rewrite heap_mapsto_vec_cons. iMod (bor_sep with "LFT H↦") as "[H↦ _]". done.
     iMod (bor_acc with "LFT H↦ Hα") as "[H↦ Hcloseα]". done.
-    wp_bind (!(LitV lx'))%E. iApply (wp_fupd_step with "[Hb]");
+    wp_bind (!(LitV lx'))%E. iApply (wp_step_fupd with "[Hb]");
       [done| |by iApply (bor_unnest with "LFT Hb")|]; first done.
     wp_read. iIntros "Hb !>". wp_let.
     iMod ("Hcloseα" with "[$H↦]") as "[_ Hα]".
@@ -135,7 +135,7 @@ Section refmut_functions.
     setoid_subst. iDestruct "INV" as (ν') "(Hνν' & H† & _)".
     iDestruct "Hνν'" as %<-%(inj to_agree)%leibniz_equiv.
     wp_bind Endlft. iApply (wp_mask_mono (↑lftN)); first done.
-    iApply (wp_fupd_step with "[H† Hν]");
+    iApply (wp_step_fupd with "[H† Hν]");
       [done| |iApply ("H†" with "Hν")|]; first set_solver.
     wp_seq. iIntros "{Hb} Hb !>".
     iMod ("Hcloseβ" with ">[H↦lrc H● H◯ Hb] Hna") as "[Hβ Hna]".
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 8a036dc71472104ce464a55040e9d98731fa29b5..1280fc24270a9927be7bdb416e40c83e560edcce 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -171,7 +171,7 @@ Section rwlock_functions.
               with "[] LFT Hna >[Hclose Hβtok1 Hβtok2] HL Hk"); first last.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
-      iApply (type_sum_assign_unit [unit; rwlockreadguard α ty]);
+      iApply (type_sum_unit [unit; rwlockreadguard α ty]);
         [solve_typing..|]; first last.
       simpl. iApply (type_jump [_]); solve_typing.
     - wp_op. wp_bind (CAS _ _ _).
@@ -283,7 +283,7 @@ Section rwlock_functions.
               with "[] LFT Hna >[Hclose Hβtok] HL Hk"); first last.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
-      iApply (type_sum_assign_unit [unit; rwlockwriteguard α ty]);
+      iApply (type_sum_unit [unit; rwlockwriteguard α ty]);
         [solve_typing..|]; first last.
       rewrite /option /=. iApply (type_jump [_]); solve_typing.
     - iApply (wp_cas_int_suc with "Hlx"). done. iIntros "!> Hlx".
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 967055edd80749b81fbee9fb021cc6058399d6e5..7e353fe1fe5ca4bfb31111f92f7940333df80ab9 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -122,7 +122,7 @@ Section rwlockreadguard_functions.
           { rewrite pos_op_plus -Pplus_one_succ_l Pos.succ_pred // =>?. by subst. }
           rewrite {1}EQn -{1}(agree_idemp (to_agree _)) -2!pair_op -Cinr_op Some_op.
           apply (cancel_local_update_empty (reading_st q ν)) , _. }
-      iApply (wp_fupd_step with "INV"). done. set_solver.
+      iApply (wp_step_fupd with "INV"). done. set_solver.
       iApply (wp_cas_int_suc with "Hlx"); try done. iNext. iIntros "Hlx INV !>".
       iMod ("INV" with "Hlx") as "INV". iMod ("Hcloseβ" with "[$INV]") as "Hβ".
       iMod ("Hcloseα" with "Hβ") as "HE". iApply (wp_if _ true). iIntros "!>!>".
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index e652202a9abb33ad59ea5edfa516326e32030a0b..9dc6b47fdf10692838c6532152c7f1b7206af33d 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -35,7 +35,7 @@ Section rwlockwriteguard_functions.
     iMod (frac_bor_acc with "LFT Hfrac Hα1") as (qlx') "[H↦ Hcloseα1]". done.
     rewrite heap_mapsto_vec_singleton.
     iDestruct (lft_intersect_acc with "Hβ Hα2") as (qβα) "[Hα2β Hcloseβα2]".
-    wp_bind (!(LitV lx'))%E. iApply (wp_fupd_step with "[Hα2β]");
+    wp_bind (!(LitV lx'))%E. iApply (wp_step_fupd with "[Hα2β]");
          [done| |by iApply ("Hshr" with "[] Hα2β")|]; first done.
     iMod "H↦" as "[H↦1 H↦2]". wp_read. iIntros "[#Hshr' Hα2β]!>". wp_op. wp_let.
     iDestruct ("Hcloseβα2" with "Hα2β") as "[Hβ Hα2]".
@@ -84,7 +84,7 @@ Section rwlockwriteguard_functions.
     iMod (bor_sep with "LFT H") as "[Hβδ _]". done.
     iMod (bor_persistent_tok with "LFT Hβδ Hα") as "[#Hβδ Hα]". done.
     iMod (bor_acc with "LFT H↦ Hα") as "[H↦ Hcloseα]". done.
-    wp_bind (!(LitV lx'))%E. iApply (wp_fupd_step with "[Hb]");
+    wp_bind (!(LitV lx'))%E. iApply (wp_step_fupd with "[Hb]");
       [done| |by iApply (bor_unnest with "LFT Hb")|]; first done.
     wp_read. iIntros "Hb !>". wp_op. wp_let.
     iMod ("Hcloseα" with "[$H↦]") as "[_ Hα]".
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index f2b6d69e7dc6255505857a9f3bb8be0c2721f1a3..cddd811915349b9d0d5d100c2486a3a6dd091155 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -171,7 +171,7 @@ Section typing_rules.
     iDestruct "Hκ" as (Λ) "(% & Htok & #Hend)".
     iSpecialize ("Hend" with "Htok"). wp_bind Endlft.
     iApply (wp_mask_mono (↑lftN)); first done.
-    iApply (wp_fupd_step with "Hend"). done. set_solver. wp_seq.
+    iApply (wp_step_fupd with "Hend"). done. set_solver. wp_seq.
     iIntros "#Hdead !>". wp_seq. iApply ("He" with "LFT Htl HE HL HC >").
     iApply (Hub with "[] HT"). simpl in *. subst κ. rewrite -lft_dead_or. auto.
   Qed.
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 2df653e81db8c502e83c2ad95c2cfd93a37c4c1e..318bb38df21d45f495561d3971e36628d096e6dd 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -180,7 +180,7 @@ Section case.
     iApply type_seq; [by eapply type_sum_assign_instr|done|done].
   Qed.
 
-  Lemma type_sum_assign_unit_instr {E L} (i : nat) tyl ty1 ty2 p :
+  Lemma type_sum_unit_instr {E L} (i : nat) tyl ty1 ty2 p :
     tyl !! i = Some unit →
     typed_write E L ty1 (sum tyl) ty2 →
     typed_instruction E L [p ◁ ty1] (p <-{Σ i} ()) (λ _, [p ◁ ty2]%TC).
@@ -195,7 +195,7 @@ Section case.
     iExists i, [], _. rewrite -Hlen nth_lookup Hty. auto.
   Qed.
 
-  Lemma type_sum_assign_unit {E L} tyl i ty1 ty1' C T T' p e:
+  Lemma type_sum_unit {E L} tyl i ty1 ty1' C T T' p e:
     Closed [] e →
     0 ≤ i →
     tctx_extract_hasty E L p ty1 T T' →
@@ -205,7 +205,7 @@ Section case.
     typed_body E L C T (p <-{Σ i} () ;; e).
   Proof.
     iIntros. rewrite -(Z2Nat.id i) //.
-    iApply type_seq; [by eapply type_sum_assign_unit_instr|solve_typing|done].
+    iApply type_seq; [by eapply type_sum_unit_instr|solve_typing|done].
   Qed.
 
   Lemma type_sum_memcpy_instr {E L} (i : nat) tyl ty1 ty1' ty2 ty2' ty p1 p2 :