diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index f1cb0b133e1e08f9f4b5bc611933f7cdc5aa759e..ec61ede5f7f3713ea4d789a473c3fc19cf6091f9 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -425,7 +425,7 @@ Section arc.
     iApply (type_new 1); [solve_typing..|]; iIntros (x); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
     iIntros (tid) "#LFT #HE Hna HL Hk [Hrcx [#Hrc' [Hx _]]]".
-    rewrite !tctx_hasty_val [[rcx]]lock.
+    rewrite !tctx_hasty_val /=.
     iDestruct (ownptr_uninit_own with "Hx") as (lrc2 vlrc2) "(% & Hx & Hx†)".
     subst x. inv_vec vlrc2=>?. rewrite heap_mapsto_vec_singleton.
     destruct rc' as [[|rc'|]|]; try done. simpl of_val.
@@ -446,7 +446,7 @@ Section arc.
     iApply (type_type _ _ _ [ rcx ◁ box (&shr{α} arc ty); #lrc2 ◁ box (&shr{α} ty)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
-      unlock. iFrame "Hrcx". iFrame "Hx†". iExists [_]. rewrite heap_mapsto_vec_singleton.
+      iFrame "Hrcx". iFrame "Hx†". iExists [_]. rewrite heap_mapsto_vec_singleton.
       iFrame "Hx". by iApply ty_shr_mono. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -469,7 +469,7 @@ Section arc.
     iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
     iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
-    rewrite !tctx_hasty_val [[x]]lock [[r]]lock.
+    rewrite !tctx_hasty_val /=.
     destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
     (* All right, we are done preparing our context. Let's get going. *)
     iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)";
@@ -490,7 +490,7 @@ Section arc.
     iApply (type_type _ _ _ [ x ◁ box (&shr{α} arc ty); #c ◁ int; r ◁ box (uninit 1)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
-      unlock. iFrame. }
+      iFrame. }
     iApply type_assign; [solve_typing..|].
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -512,7 +512,7 @@ Section arc.
     iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
     iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
-    rewrite !tctx_hasty_val [[x]]lock [[r]]lock.
+    rewrite !tctx_hasty_val /=.
     destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
     (* All right, we are done preparing our context. Let's get going. *)
     iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)";
@@ -533,7 +533,7 @@ Section arc.
     iApply (type_type _ _ _ [ x ◁ box (&shr{α} arc ty); #c ◁ int; r ◁ box (uninit 1)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
-      unlock. iFrame. }
+      iFrame. }
     iApply type_assign; [solve_typing..|].
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -557,7 +557,7 @@ Section arc.
     iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
     iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
-    rewrite !tctx_hasty_val [[x]]lock [[r]]lock.
+    rewrite !tctx_hasty_val /=.
     destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
     (* All right, we are done preparing our context. Let's get going. *)
     iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)";
@@ -578,7 +578,7 @@ Section arc.
     iApply (type_type _ _ _ [ x ◁ box (&shr{α} arc ty); #l' ◁ arc ty; r ◁ box (uninit 1)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
-      unlock. iFrame. simpl. unfold shared_arc_own. auto 10 with iFrame. }
+      iFrame. simpl. unfold shared_arc_own. auto 10 with iFrame. }
     iApply type_assign; [solve_typing..|].
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -601,7 +601,7 @@ Section arc.
     iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
     iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
-    rewrite !tctx_hasty_val [[x]]lock [[r]]lock.
+    rewrite !tctx_hasty_val /=.
     destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
     (* All right, we are done preparing our context. Let's get going. *)
     iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)";
@@ -622,7 +622,7 @@ Section arc.
     iApply (type_type _ _ _ [ x ◁ box (&shr{α} weak ty); #l' ◁ weak ty; r ◁ box (uninit 1) ]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
-      unlock. iFrame. simpl. eauto 10 with iFrame. }
+      iFrame. simpl. eauto 10 with iFrame. }
     iApply type_assign; [solve_typing..|].
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -645,7 +645,7 @@ Section arc.
     iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
     iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
-    rewrite !tctx_hasty_val [[x]]lock [[r]]lock.
+    rewrite !tctx_hasty_val /=.
     destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
     (* All right, we are done preparing our context. Let's get going. *)
     iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)";
@@ -666,7 +666,7 @@ Section arc.
     iApply (type_type _ _ _ [ x ◁ box (&shr{α} arc ty); #l' ◁ weak ty; r ◁ box (uninit 1) ]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
-      unlock. iFrame. simpl. eauto 10 with iFrame. }
+      iFrame. simpl. eauto 10 with iFrame. }
     iApply type_assign; [solve_typing..|].
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -692,7 +692,7 @@ Section arc.
     iApply (type_new 2); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
     iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
-    rewrite !tctx_hasty_val [[x]]lock [[r]]lock.
+    rewrite !tctx_hasty_val /=.
     destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
     (* All right, we are done preparing our context. Let's get going. *)
     iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)";
@@ -714,7 +714,7 @@ Section arc.
                                 r ◁ box (uninit 2) ]
               with "[] LFT HE Hna HL Hk [-]"); last first.
       { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
-        unlock. iFrame. simpl. unfold shared_arc_own. eauto 10 with iFrame. }
+        iFrame. simpl. unfold shared_arc_own. eauto 10 with iFrame. }
       iApply (type_sum_assign (option (arc ty))); [solve_typing..|].
       iApply type_delete; [solve_typing..|].
       iApply type_jump; solve_typing.
@@ -722,7 +722,7 @@ Section arc.
       iApply (type_type _ _ _ [ x ◁ box (&shr{α} weak ty); r ◁ box (uninit 2) ]
               with "[] LFT HE Hna HL Hk [-]"); last first.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
-        unlock. iFrame. }
+        iFrame. }
       iApply (type_sum_unit (option (arc ty))); [solve_typing..|].
       iApply type_delete; [solve_typing..|].
       iApply type_jump; solve_typing.
@@ -751,7 +751,7 @@ Section arc.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
     iApply (type_sum_unit (option ty)); [solve_typing..|].
     iIntros (tid) "#LFT #HE Hna HL Hk [Hr [Hrcx [Hrc' _]]]".
-    rewrite !tctx_hasty_val [[rcx]]lock [[r]]lock. destruct rc' as [[|rc'|]|]=>//=.
+    rewrite !tctx_hasty_val /=. destruct rc' as [[|rc'|]|]=>//=.
     iAssert (shared_arc_own rc' ty tid)%I with "[>Hrc']" as "Hrc'".
     { iDestruct "Hrc'" as "[?|$]"; last done. iApply arc_own_share; solve_ndisj. }
     iDestruct "Hrc'" as (γ ν q) "(#Hpersist & Htok & Hν)".
@@ -759,7 +759,7 @@ Section arc.
       [by iDestruct "Hpersist" as "[$?]"|done|].
     iNext. iIntros (b) "Hdrop". wp_bind (if: _ then _ else _)%E.
     iApply (wp_wand _ _ (λ _, ty_own (box (option ty)) tid [r])%I with "[Hdrop Hr]").
-    { unlock. destruct b; wp_if=>//. destruct r as [[]|]=>//=.
+    { destruct b; wp_if=>//. destruct r as [[]|]=>//=.
       iDestruct "Hr" as "[Hr ?]". iDestruct "Hr" as ([|d vl]) "[H↦ Hown]";
         first by iDestruct "Hown" as (???) "[>% ?]".
       rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[H↦0 H↦1]".
@@ -787,7 +787,7 @@ Section arc.
     (* Finish up the proof. *)
     iApply (type_type _ _ _ [ rcx ◁ box (uninit 1); r ◁ box (option ty) ]
             with "[] LFT HE Hna HL Hk [-]"); last first.
-    { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val. unlock. iFrame.
+    { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val. iFrame.
       by rewrite tctx_hasty_val. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -809,7 +809,7 @@ Section arc.
     iApply (type_new 0); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
     iIntros (tid) "#LFT #HE Hna HL Hk [Hrcx [Hrc' [Hr _]]]".
-    rewrite !tctx_hasty_val [[rcx]]lock [[r]]lock. destruct rc' as [[|rc'|]|]=>//=.
+    rewrite !tctx_hasty_val /=. destruct rc' as [[|rc'|]|]=>//=.
     iDestruct "Hrc'" as (γ ν) "[#Hpersist Htok]". wp_bind (drop_weak _).
     iApply (drop_weak_spec with "[] [Htok]"); [by iDestruct "Hpersist" as "[$?]"|by auto|].
     iIntros "!> * Hdrop". wp_bind (if: _ then _ else _)%E.
@@ -822,7 +822,7 @@ Section arc.
     (* Finish up the proof. *)
     iApply (type_type _ _ _ [ rcx ◁ box (uninit 1); r ◁ box unit ]
             with "[] LFT HE Hna HL Hk [-]"); last first.
-    { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val. unlock. iFrame.
+    { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val. iFrame.
       by rewrite tctx_hasty_val. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -853,14 +853,14 @@ Section arc.
       [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
     iIntros (tid) "#LFT #HE Hna HL Hk [Hrcx [Hrc' [Hr _]]]".
-    rewrite !tctx_hasty_val [[rcx]]lock [[r]]lock. destruct rc' as [[|rc'|]|]=>//=.
+    rewrite !tctx_hasty_val /=. destruct rc' as [[|rc'|]|]=>//=.
     iAssert (shared_arc_own rc' ty tid)%I with "[>Hrc']" as "Hrc'".
     { iDestruct "Hrc'" as "[?|$]"; last done. iApply arc_own_share; solve_ndisj. }
     iDestruct "Hrc'" as (γ ν q) "(#Hpersist & Htok & Hν)".
     wp_apply (try_unwrap_spec with "[] [Hν Htok]");
       [by iDestruct "Hpersist" as "[$?]"|iFrame|].
     iIntros ([]) "H"; wp_if.
-    - iDestruct "H" as "[Hν Hend]". rewrite -(lock [r]). destruct r as [[|r|]|]=>//=.
+    - iDestruct "H" as "[Hν Hend]". destruct r as [[|r|]|]=>//=.
       iDestruct "Hr" as "[Hr >Hfree]". iDestruct "Hr" as (vl0) "[>Hr Hown]".
       rewrite uninit_own. iDestruct "Hown" as ">Hlen".
       destruct vl0 as [|? vl0]=>//; iDestruct "Hlen" as %[=Hlen0].
@@ -885,7 +885,7 @@ Section arc.
       iIntros (?) "_". wp_seq.
       iApply (type_type _ _ _ [ rcx ◁ box (uninit 1); #r ◁ box (Σ[ ty; arc ty ]) ]
               with "[] LFT HE Hna HL Hk [-]"); last first.
-      { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val. unlock.
+      { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val.
         iFrame. iCombine "Hr1" "Hr2" as "Hr1". iCombine "Hr0" "Hr1" as "Hr".
         rewrite -[in shift_loc _ ty.(ty_size)]Hlen -heap_mapsto_vec_app
                 -heap_mapsto_vec_cons tctx_hasty_val' //. iFrame. iExists _. iFrame.
@@ -897,7 +897,7 @@ Section arc.
                                 r ◁ box (uninit (Σ[ ty; arc ty ]).(ty_size)) ]
               with "[] LFT HE Hna HL Hk [-]"); last first.
       { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
-        unlock. iFrame. iRight. iExists _, _, _. auto with iFrame. }
+        iFrame. iRight. iExists _, _, _. auto with iFrame. }
       iApply (type_sum_assign Σ[ ty; arc ty ]); [solve_typing..|].
       iApply type_delete; [solve_typing..|].
       iApply type_jump; solve_typing.
@@ -925,7 +925,7 @@ Section arc.
     iApply (type_new 2); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
     iIntros (tid) "#LFT #HE Hna HL Hk [Hrcx [Hrc' [Hr _]]]".
-    rewrite !tctx_hasty_val [[rcx]]lock [[r]]lock. destruct rc' as [[|rc'|]|]=>//=.
+    rewrite !tctx_hasty_val /=. destruct rc' as [[|rc'|]|]=>//=.
     iMod (lctx_lft_alive_tok α with "HE HL") as (q) "(Hα & HL & Hclose1)";
       [solve_typing..|].
     iMod (bor_exists with "LFT Hrc'") as (rcvl) "Hrc'"=>//.
@@ -950,7 +950,7 @@ Section arc.
                                 r ◁ box (uninit 2) ]
               with "[] LFT HE Hna HL Hk [-]"); last first.
       { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
-                tctx_hasty_val' //. unlock. iFrame. }
+                tctx_hasty_val' //. iFrame. }
       iApply (type_sum_assign (option (&uniq{α}ty))); [solve_typing..|].
       iApply type_delete; [solve_typing..|].
       iApply type_jump; solve_typing.
@@ -959,7 +959,7 @@ Section arc.
       iMod ("Hclose1" with "Hα HL") as "HL".
       iApply (type_type _ _ _ [ rcx ◁ box (uninit 1); r ◁ box (uninit 2) ]
               with "[] LFT HE Hna HL Hk [-]"); last first.
-      { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. unlock. iFrame. }
+      { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
       iApply (type_sum_unit (option (&uniq{α}ty))); [solve_typing..|].
       iApply type_delete; [solve_typing..|].
       iApply type_jump; solve_typing.
@@ -1013,7 +1013,7 @@ Section arc.
     iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
     iIntros (tid) "#LFT #HE Hna HL Hk [Hrcx [Hrc' [Hr _]]]".
-    rewrite !tctx_hasty_val [[rcx]]lock [[r]]lock. destruct rc' as [[|rc'|]|]=>//=.
+    rewrite !tctx_hasty_val /=. destruct rc' as [[|rc'|]|]=>//=.
     iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)";
       [solve_typing..|].
     iMod (bor_acc_cons with "LFT Hrc' Hα1") as "[Hrc' Hclose2]"=>//.
@@ -1037,7 +1037,7 @@ Section arc.
                                 r ◁ box (uninit 1) ]
               with "[] LFT HE Hna HL Hk [-]"); last first.
       { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
-                tctx_hasty_val' //. unlock. iFrame. }
+                 tctx_hasty_val' //. iFrame. }
       iApply type_assign; [solve_typing..|].
       iApply type_delete; [solve_typing..|].
       iApply type_jump; solve_typing.
@@ -1061,7 +1061,7 @@ Section arc.
                                 r ◁ box (uninit 1) ]
               with "[] LFT HE Hna HL Hk [-]"); last first.
       { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
-                tctx_hasty_val' //. unlock. iFrame. }
+                tctx_hasty_val' //. iFrame. }
       iApply type_assign; [solve_typing..|].
       iApply type_delete; [solve_typing..|].
       iApply type_jump; solve_typing.
@@ -1129,7 +1129,7 @@ Section arc.
                                 r ◁ box (uninit 1); rcx ◁ box (uninit 1) ]
               with "[] LFT HE Hna HL Hk [-]"); last first.
       { rewrite 3!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
-                !tctx_hasty_val' //. unlock. iFrame. iRight.
+                !tctx_hasty_val' //. iFrame. iRight.
         iExists _, _, _. iFrame "∗#". }
       iApply type_letalloc_1; [solve_typing..|]. iIntros (rcold). simpl_subst.
       iApply type_let. apply arc_drop_type. solve_typing. iIntros (drop). simpl_subst.
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index f97d1eb696e046618f3b98b87214d55975eec44c..7dfd6b6b3137cbf1e379ecb09c6d3ff1a7e1a43d 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -225,7 +225,7 @@ Section code.
     iApply type_deref; [solve_typing..|]; iIntros (m'); simpl_subst.
     (* Go to Iris *)
     iIntros (tid) "#LFT #HE Hna HL Hk [Hm [Hm' _]]".
-    rewrite !tctx_hasty_val [[m]]lock.
+    rewrite !tctx_hasty_val /=.
     destruct m' as [[|lm'|]|]; try done. simpl.
     iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose1)";
       [solve_typing..|].
@@ -243,7 +243,7 @@ Section code.
     iApply (type_type _ _ _ [ m ◁ own_ptr _ _; #(shift_loc lm' 1) ◁ &uniq{α} ty]
         with "[] LFT HE Hna HL Hk"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
-      unlock. iFrame. }
+      iFrame. }
     iApply type_assign; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index 1ecf688eb58c9cd41c0924e0b96186728bd04e63..22cd8165d30144d4e6a76777cfcd9848c24ff2dd 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -167,7 +167,7 @@ Section code.
     iApply (type_new 1); [solve_typing..|]; iIntros (g); simpl_subst.
     (* Switch to Iris. *)
     iIntros (tid) "#LFT #HE Hna HL Hk [Hg [Hx [Hm _]]]".
-    rewrite !tctx_hasty_val [[x]]lock /=.
+    rewrite !tctx_hasty_val /=.
     destruct m as [[|lm|]|]; try done. iDestruct "Hm" as (γ κ') "[#Hshr #Hακ']".
     iDestruct (ownptr_uninit_own with "Hg") as (lg vlg) "(% & Hg & Hg†)".
     subst g. inv_vec vlg=>g. rewrite heap_mapsto_vec_singleton.
@@ -181,7 +181,7 @@ Section code.
         with "[] LFT HE Hna HL Hk"); last first.
     (* TODO: It would be nice to say [{#}] as the last spec pattern to clear the context in there. *)
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
-      unlock. iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame "Hg".
+      iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame "Hg".
       iExists _, _. iFrame "#∗". }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -203,7 +203,7 @@ Section code.
     iApply type_deref; [solve_typing..|]; iIntros (g'); simpl_subst.
     (* Switch to Iris. *)
     iIntros (tid) "#LFT #HE Hna HL Hk [Hg [Hg' _]]".
-    rewrite !tctx_hasty_val [[g]]lock /=.
+    rewrite !tctx_hasty_val /=.
     destruct g' as [[|lg|]|]; try done. simpl.
     iMod (bor_exists with "LFT Hg'") as (vl) "Hbor"; first done.
     iMod (bor_sep with "LFT Hbor") as "[H↦ Hprot]"; first done.
@@ -229,7 +229,7 @@ Section code.
     iApply (type_type _ _ _ [ g ◁ own_ptr _ _; #lm +ₗ #1 ◁ &uniq{α} ty ]
         with "[] LFT HE Hna HL Hk"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
-      unlock. iFrame. iApply bor_shorten; last done.
+      iFrame. iApply bor_shorten; last done.
       iApply lft_incl_glb; last by iApply lft_incl_refl.
       iApply lft_incl_trans; done. }
     iApply type_letalloc_1; [solve_typing..|]; iIntros (r); simpl_subst.
@@ -248,7 +248,7 @@ Section code.
     iApply type_deref; [solve_typing..|]; iIntros (g'); simpl_subst.
     (* Switch to Iris. *)
     iIntros (tid) "#LFT #HE Hna HL Hk [Hg [Hg' _]]".
-    rewrite !tctx_hasty_val [[g]]lock /=.
+    rewrite !tctx_hasty_val /=.
     destruct g' as [[|lg|]|]; try done. simpl.
     iDestruct "Hg'" as (lm) "[Hlg Hshr]".
     iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "([Hα1 Hα2] & HL & Hclose1)";
@@ -269,7 +269,7 @@ Section code.
     iApply (type_type _ _ _ [ g ◁ own_ptr _ _; #lm +ₗ #1 ◁ &shr{α} ty ]
         with "[] LFT HE Hna HL Hk"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
-      unlock. iFrame. iApply ty_shr_mono; last done.
+      iFrame. iApply ty_shr_mono; last done.
       iApply lft_incl_glb; last by iApply lft_incl_refl. done. }
     iApply type_letalloc_1; [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_delete; [solve_typing..|].
@@ -291,7 +291,7 @@ Section code.
     iApply type_deref; [solve_typing..|]; iIntros (m); simpl_subst.
     (* Switch to Iris. *)
     iIntros (tid) "#LFT #HE Hna HL Hk [Hg [Hm _]]".
-    rewrite !tctx_hasty_val [[g]]lock /=.
+    rewrite !tctx_hasty_val /=.
     destruct m as [[|lm|]|]; try done. iDestruct "Hm" as (γ β) "(Hlcked & #Hαβ & #Hshr & Hcnt)".
     (* All right, we are done preparing our context. Let's get going. *)
     iMod (lctx_lft_alive_tok α with "HE HL") as (q) "(Hα & HL & Hclose1)"; [solve_typing..|].
@@ -301,7 +301,7 @@ Section code.
     (* Switch back to typing mode. *)
     iApply (type_type _ _ _ [ g ◁ own_ptr _ _ ]
         with "[] LFT HE Hna HL Hk"); last first.
-    { rewrite tctx_interp_singleton tctx_hasty_val. unlock. iFrame. }
+    { rewrite tctx_interp_singleton tctx_hasty_val. iFrame. }
     iApply type_delete; [solve_typing..|].
     iApply type_new; [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_jump; solve_typing.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 2005139343c881ae8dd2f5b34d57f087981bf36c..a6d02f63f1371f6710147e2aed0372bf9fa8b26c 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -386,7 +386,7 @@ Section code.
     iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
     iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
-    rewrite !tctx_hasty_val [[x]]lock [[r]]lock.
+    rewrite !tctx_hasty_val /=.
     destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
     (* All right, we are done preparing our context. Let's get going. *)
     iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)"; [solve_typing..|].
@@ -418,8 +418,7 @@ Section code.
     iApply (type_type _ _ _ [ x ◁ box (&shr{α} rc ty); r ◁ box (uninit 1);
                               #(Z.pos s0) ◁ int ]
         with "[] LFT HE Hna HL Hk [-]"); last first.
-    { unlock.
-      rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
+    { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
       iFrame. }
     iApply type_assign; [solve_typing..|].
     iApply type_delete; [solve_typing..|].
@@ -445,7 +444,7 @@ Section code.
     iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
     iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
-    rewrite !tctx_hasty_val [[x]]lock [[r]]lock.
+    rewrite !tctx_hasty_val /=.
     destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
     (* All right, we are done preparing our context. Let's get going. *)
     iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)"; [solve_typing..|].
@@ -477,8 +476,7 @@ Section code.
     iApply (type_type _ _ _ [ x ◁ box (&shr{α} rc ty); r ◁ box (uninit 1);
                               #(S weak) ◁ int ]
         with "[] LFT HE Hna HL Hk [-]"); last first.
-    { unlock.
-      rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
+    { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
       iFrame. }
     iApply type_int. iIntros (?). simpl_subst.
     iApply type_minus; [solve_typing..|]. iIntros (?). simpl_subst.
@@ -548,7 +546,7 @@ Section code.
     iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
     iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
-    rewrite !tctx_hasty_val [[x]]lock.
+    rewrite !tctx_hasty_val /=.
     destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
     iDestruct (ownptr_uninit_own with "Hr") as (lr vlr) "(% & Hr & Hr†)".
     subst r. inv_vec vlr=>r. rewrite heap_mapsto_vec_singleton.
@@ -590,7 +588,7 @@ Section code.
     iApply (type_type _ _ _ [ x ◁ box (&shr{α} rc ty); #lr ◁ box (rc ty)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
-      unlock. iFrame "Hx". iFrame "Hr†". iExists [# #l'].
+      iFrame "Hx Hr†". iExists [# #l'].
       rewrite heap_mapsto_vec_singleton /=. simpl. eauto 10 with iFrame. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -611,7 +609,7 @@ Section code.
     iApply (type_new 1); [solve_typing..|]; iIntros (x); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
     iIntros (tid) "#LFT #HE Hna HL Hk [Hrcx [#Hrc' [Hx _]]]".
-    rewrite !tctx_hasty_val [[rcx]]lock.
+    rewrite !tctx_hasty_val /=.
     iDestruct (ownptr_uninit_own with "Hx") as (lrc2 vlrc2) "(% & Hx & Hx†)".
     subst x. inv_vec vlrc2=>?. rewrite heap_mapsto_vec_singleton.
     destruct rc' as [[|rc'|]|]; try done. simpl of_val.
@@ -632,7 +630,7 @@ Section code.
     iApply (type_type _ _ _ [ rcx ◁ box (&shr{α} rc ty); #lrc2 ◁ box (&shr{α} ty)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
-      unlock. iFrame "Hrcx". iFrame "Hx†". iExists [_]. rewrite heap_mapsto_vec_singleton.
+      iFrame "Hrcx Hx†". iExists [_]. rewrite heap_mapsto_vec_singleton.
       iFrame "Hx". by iApply ty_shr_mono. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -681,7 +679,7 @@ Section code.
     iIntros (k). simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
     iIntros (tid) "#LFT #HE Hna HL Hk [Hrcx [Hrc' [Hr _]]]".
-    rewrite !tctx_hasty_val [[rcx]]lock [[r]]lock.
+    rewrite !tctx_hasty_val /=.
     destruct rc' as [[|rc'|]|]; try done.
     rewrite [[ #rc' ]]lock. wp_op. rewrite shift_loc_0 -(lock [ #rc' ]).
     wp_apply (rc_check_unique with "[$Hna $Hrc']"); first solve_ndisj.
@@ -697,7 +695,7 @@ Section code.
       iApply (wp_wand with "[Hna HL Hty Hr H†2]").
       { iApply (type_sum_memcpy_instr 0 [_; (rc ty)] with "LFT HE Hna HL"); first done.
         { by eapply (write_own _ (uninit _)). } { apply read_own_move. }
-        iSplitL "Hr"; first by unlock; rewrite tctx_hasty_val. iSplitL; last done.
+        iSplitL "Hr"; first by rewrite tctx_hasty_val. iSplitL; last done.
         rewrite tctx_hasty_val'; last done. iFrame. }
       iIntros (?) "(Hna & HL & [Hr [Hrc _]])". wp_seq.
       iMod ("Hproto" with "Hna") as (weak) "[H↦weak Hproto]". wp_op. wp_read. wp_let.
@@ -709,7 +707,7 @@ Section code.
                #rc' +ₗ #2 ◁ own_ptr (2 + ty.(ty_size)) (uninit (ty.(ty_size)));
                #rc' +ₗ #0 ◁ own_ptr (2 + ty.(ty_size)) (uninit 2)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
-        { unlock. rewrite 3!tctx_interp_cons tctx_interp_singleton. iFrame "Hr Hrc".
+        { rewrite 3!tctx_interp_cons tctx_interp_singleton. iFrame "Hr Hrc".
           rewrite 1!tctx_hasty_val tctx_hasty_val' //. iFrame "Hrcx".
           rewrite shift_loc_0 /=. iFrame. iExists [_; _].
           rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton uninit_own.
@@ -724,14 +722,14 @@ Section code.
              [ r ◁ own_ptr (ty_size Σ[ ty; rc ty ]) (Σ[ ty; rc ty]);
                rcx ◁ box (uninit 1) ]
         with "[] LFT HE Hna HL Hk [-]"); last first.
-        { unlock. rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
+        { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
         iApply type_jump; solve_typing.
     - wp_op; intros Hc; first lia. wp_if. iMod ("Hproto" with "Hrc") as "[Hna Hrc]".
       iApply (type_type _ _ _ [ r ◁ own_ptr (ty_size Σ[ ty; rc ty ]) (uninit _);
                                 rcx ◁ box (uninit 1); #rc' ◁ rc ty ]
         with "[] LFT HE Hna HL Hk [-]"); last first.
       { rewrite 2!tctx_interp_cons tctx_interp_singleton.
-        rewrite !tctx_hasty_val tctx_hasty_val' //. unlock. iFrame. }
+        rewrite !tctx_hasty_val tctx_hasty_val' //. iFrame. }
       iApply (type_sum_assign Σ[ ty; rc ty ]); [solve_typing..|].
       iApply type_jump; solve_typing.
   Qed.
@@ -776,7 +774,7 @@ Section code.
     iIntros (k). simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
     iIntros (tid) "#LFT #HE Hna HL Hk [Hrcx [Hrc' [Hr _]]]".
-    rewrite !tctx_hasty_val [[rcx]]lock [[r]]lock.
+    rewrite !tctx_hasty_val /=.
     destruct rc' as [[|rc'|]|]; try done. rewrite [[ #rc' ]]lock.
     wp_op. rewrite shift_loc_0. rewrite -(lock [ #rc' ]).
     wp_apply (rc_check_unique with "[$Hna $Hrc']"); first solve_ndisj.
@@ -792,7 +790,7 @@ Section code.
       iApply (wp_wand with "[Hna HL Hty Hr H†2]").
       { iApply (type_sum_memcpy_instr 1 [unit; _] with "LFT HE Hna HL"); first done.
         { by eapply (write_own _ (uninit _)). } { apply read_own_move. }
-        iSplitL "Hr"; first by unlock; rewrite tctx_hasty_val. iSplitL; last done.
+        iSplitL "Hr"; first by rewrite tctx_hasty_val. iSplitL; last done.
         rewrite tctx_hasty_val'; last done. iFrame. }
       iIntros (?) "(Hna & HL & [Hr [Hrc _]])". wp_seq.
       iMod ("Hproto" with "Hna") as (weak) "[H↦weak Hproto]". wp_op. wp_read. wp_let.
@@ -804,7 +802,7 @@ Section code.
                #rc' +ₗ #2 ◁ own_ptr (2 + ty.(ty_size)) (uninit (ty.(ty_size)));
                #rc' +ₗ #0 ◁ own_ptr (2 + ty.(ty_size)) (uninit 2)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
-        { unlock. rewrite 3!tctx_interp_cons tctx_interp_singleton. iFrame "Hr Hrc".
+        { rewrite 3!tctx_interp_cons tctx_interp_singleton. iFrame "Hr Hrc".
           rewrite 1!tctx_hasty_val tctx_hasty_val' //. iFrame "Hrcx".
           rewrite shift_loc_0 /=. iFrame. iExists [_; _].
           rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton uninit_own.
@@ -818,7 +816,7 @@ Section code.
         iApply (type_type _ _ _
              [ r ◁ own_ptr (ty_size (option ty)) (option ty); rcx ◁ box (uninit 1) ]
         with "[] LFT HE Hna HL Hk [-]"); last first.
-        { unlock. rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
+        { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
         iApply type_jump; solve_typing.
     - wp_op; intros Hc; first lia. wp_if. iMod ("Hproto" with "Hrc") as "Hna".
       iApply (type_type _ _ _ [ r ◁ own_ptr (ty_size (option ty)) (uninit _);
@@ -866,7 +864,7 @@ Section code.
     iIntros (k). simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
     iIntros (tid) "#LFT #HE Hna HL Hk [Hrcx [Hrc' [Hr _]]]".
-    rewrite !tctx_hasty_val  [[rcx]]lock [[r]]lock.
+    rewrite !tctx_hasty_val /=.
     destruct rc' as [[|rc'|]|]; try done.
     iMod (lctx_lft_alive_tok α with "HE HL") as (q) "(Hα & HL & Hclose1)"; [solve_typing..|].
     iMod (bor_acc_cons with "LFT Hrc' Hα") as "[Hrc' Hclose2]"; first solve_ndisj.
@@ -891,7 +889,7 @@ Section code.
                                   rcx ◁ box (uninit 1)]
                 with "[] LFT HE Hna HL Hk [-]"); last first.
         { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
-          unlock. iFrame. }
+          iFrame. }
         iApply (type_sum_assign (option (&uniq{_} _))); [solve_typing..|].
         iApply type_jump; solve_typing.
       + wp_op=>[?|_]; first lia. wp_if. iMod ("Hrc" with "Hl1 Hl2") as "[Hna Hrc]".
@@ -902,7 +900,7 @@ Section code.
         iApply (type_type _ _ _ [ r ◁ box (uninit 2); rcx ◁ box (uninit 1)]
                 with "[] LFT HE Hna HL Hk [-]"); last first.
         { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
-          unlock. iFrame. }
+          iFrame. }
         iApply (type_sum_unit (option (&uniq{_} _))); [solve_typing..|].
         iApply type_jump; solve_typing.
     - wp_if. iDestruct "Hc" as "[[% _]|[% [Hproto _]]]"; first lia.
@@ -914,7 +912,7 @@ Section code.
       iApply (type_type _ _ _ [ r ◁ box (uninit 2); rcx ◁ box (uninit 1)]
               with "[] LFT HE Hna HL Hk [-]"); last first.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
-        unlock. iFrame. }
+        iFrame. }
       iApply (type_sum_unit (option (&uniq{_} _))); [solve_typing..|].
       iApply type_jump; solve_typing.
   Qed.
@@ -1004,7 +1002,7 @@ Section code.
              rc' ◁{β} &uniq{α} rc ty; r ◁ own_ptr 1 (uninit 1)]);
       [simpl; solve_typing|done|].
     iIntros (tid) "#LFT #HE Hna HL Hk [Hrc' [Hrcx [Hrc'h [Hr _]]]]".
-    rewrite !tctx_hasty_val [[rcx]]lock [[r]]lock.
+    rewrite !tctx_hasty_val /=.
     destruct rc' as [[|rc'|]|]; try done.
     iMod (lctx_lft_alive_tok β with "HE HL") as (q) "(Hβ & HL & Hclose1)"; [solve_typing..|].
     iMod (bor_acc_cons with "LFT Hrc' Hβ") as "[Hrc' Hclose2]"; first solve_ndisj.
@@ -1028,7 +1026,7 @@ Section code.
                                   rcx ◁ box (uninit 1)]
                 with "[] LFT HE Hna HL Hk [-]"); last first.
         { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
-          unlock. iFrame. }
+          iFrame. }
         iApply type_assign; [solve_typing..|].
         iApply type_equivalize_lft.
         iApply type_jump; solve_typing.
@@ -1052,7 +1050,7 @@ Section code.
                                   rcx ◁ box (uninit 1)]
                 with "[] LFT HE Hna HL Hk [-]"); last first.
         { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
-                  tctx_hasty_val' //. unlock. iFrame. }
+                  tctx_hasty_val' //. iFrame. }
         iApply type_assign; [solve_typing..|].
         iApply type_equivalize_lft.
         iApply type_jump; solve_typing.
@@ -1083,14 +1081,14 @@ Section code.
                                 #rc' ◁{β} &uniq{α} rc ty; rcx ◁ box (uninit 1)]
               with "[] LFT HE Hna HL Hk [-]"); last first.
       { rewrite 3!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
-                  tctx_hasty_val' //. unlock. iFrame.
+                  tctx_hasty_val' //. iFrame.
         rewrite /= freeable_sz_full_S. iFrame. iExists [_].
         rewrite heap_mapsto_vec_singleton /=. auto with iFrame. }
       iApply type_let; [apply Hclone|solve_typing|]. iIntros (clonev). simpl_subst.
       iApply type_letcall; [solve_typing..|]. iIntros (cl). simpl_subst.
       iApply type_endlft.
       clear tid q. iIntros (tid) "_ _ Hna HL Hk [Hcl [_ [Hr [Hrc' [Hrcx _]]]]]".
-      rewrite !tctx_hasty_val [[r]]lock [[rcx]]lock ownptr_own tctx_hasty_val' //.
+      rewrite !tctx_hasty_val /= ownptr_own tctx_hasty_val' //=.
       iDestruct "Hcl" as (lcl vlcl) "(% & Hlcl & Hvlcl & Hclfree)". subst.
       iDestruct (ty_size_eq with "Hvlcl") as "#>Heq".
       iDestruct "Heq" as %Htysize. wp_apply wp_new; first lia.
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index abb7fe90d78d2c2428c6f450531351a03014853a..cd9bf7036081ba8b6a619a0cef39c3faa1f76547 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -139,7 +139,7 @@ Section code.
     iIntros (k). simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (w'); simpl_subst.
     iIntros (tid) "#LFT #HE Hna HL Hk [Hw [Hw' [Hr _]]]".
-    rewrite !tctx_hasty_val [[w]]lock.
+    rewrite !tctx_hasty_val /=.
     destruct w' as [[|lw|]|]; try done. iDestruct "Hw'" as (l') "[#Hlw #Hshr]".
     iDestruct (ownptr_uninit_own with "Hr") as (lr vlr) "(% & Hr & Hr†)".
     subst r. inv_vec vlr=>r0 r1. rewrite !heap_mapsto_vec_cons.
@@ -184,7 +184,7 @@ Section code.
                                 #l' ◁ rc ty ]
           with "[] LFT HE Hna HL Hk [-]"); last first.
       { rewrite 2!tctx_interp_cons tctx_interp_singleton tctx_hasty_val !tctx_hasty_val' //.
-        unlock. iFrame "Hr† Hw". iSplitL "Hr1 Hr2".
+        iFrame "Hr† Hw". iSplitL "Hr1 Hr2".
         - setoid_rewrite uninit_own. iExists [_;_].
           rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton. auto with iFrame.
         - iRight. auto with iFrame. }
@@ -202,7 +202,7 @@ Section code.
       iApply (type_type _ _ _ [ w ◁ box (&shr{α} weak ty); #lr ◁ box (uninit 2) ]
           with "[] LFT HE Hna HL Hk [-]"); last first.
       { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
-        unlock. iFrame. setoid_rewrite uninit_own. iExists [_;_].
+        iFrame. setoid_rewrite uninit_own. iExists [_;_].
         rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton. auto with iFrame. }
       iApply (type_sum_unit (option (rc ty))); [solve_typing..|].
       iApply type_jump; solve_typing.
@@ -218,7 +218,7 @@ Section code.
       iApply (type_type _ _ _ [ w ◁ box (&shr{α} weak ty); #lr ◁ box (uninit 2) ]
           with "[] LFT HE Hna HL Hk [-]"); last first.
       { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
-        unlock. iFrame. setoid_rewrite uninit_own. iExists [_;_].
+        iFrame. setoid_rewrite uninit_own. iExists [_;_].
         rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton. auto with iFrame. }
       iApply (type_sum_unit (option (rc ty))); [solve_typing..|].
       iApply type_jump; solve_typing.
@@ -243,7 +243,7 @@ Section code.
     iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
     iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
-    rewrite !tctx_hasty_val [[x]]lock.
+    rewrite !tctx_hasty_val /=.
     destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
     iDestruct (ownptr_uninit_own with "Hr") as (lr vlr) "(% & Hr & Hr†)".
     subst r. inv_vec vlr=>r. rewrite heap_mapsto_vec_singleton.
@@ -279,7 +279,7 @@ Section code.
     iApply (type_type _ _ _ [ x ◁ box (&shr{α} rc ty); #lr ◁ box (weak ty)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
-      unlock. iFrame "Hx". iFrame "Hr†". iExists [# #l'].
+      iFrame "Hx Hr†". iExists [# #l'].
       rewrite heap_mapsto_vec_singleton /=. eauto 10 with iFrame. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -305,7 +305,7 @@ Section code.
     iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
     iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
-    rewrite !tctx_hasty_val [[x]]lock.
+    rewrite !tctx_hasty_val /=.
     destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
     iDestruct (ownptr_uninit_own with "Hr") as (lr vlr) "(% & Hr & Hr†)".
     subst r. inv_vec vlr=>r. rewrite heap_mapsto_vec_singleton.
@@ -352,7 +352,7 @@ Section code.
     iApply (type_type _ _ _ [ x ◁ box (&shr{α} weak ty); #lr ◁ box (weak ty)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
-      unlock. iFrame. iExists [# #l']. rewrite heap_mapsto_vec_singleton /=.
+      iFrame. iExists [# #l']. rewrite heap_mapsto_vec_singleton /=.
       auto 10 with iFrame. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -387,7 +387,7 @@ Section code.
     iIntros (k). simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (w'); simpl_subst.
     iIntros (tid) "#LFT #HE Hna HL Hk [Hw [Hw' _]]".
-    rewrite !tctx_hasty_val [[w]]lock. destruct w' as [[|lw|]|]; try done. wp_op.
+    rewrite !tctx_hasty_val /=. destruct w' as [[|lw|]|]; try done. wp_op.
     iDestruct "Hw'" as (γ ν) "[#Hpersist Hwtok]".
     iAssert (∃ wv : Z, shift_loc lw 1 ↦ #wv ∗
         ((⌜wv = 1⌝ ∗ na_own tid ⊤ ∗
@@ -425,7 +425,7 @@ Section code.
       iApply (type_type _ _ _ [ w ◁ box (uninit 1); #lw ◁ box (uninit (2 + ty.(ty_size))) ]
               with "[] LFT HE Hna HL Hk [-]"); last first.
       { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
-        unlock. iFrame. iDestruct "H" as (?) "(? & H↦ & ?)". iDestruct "H↦" as (?) "[? %]".
+        iFrame. iDestruct "H" as (?) "(? & H↦ & ?)". iDestruct "H↦" as (?) "[? %]".
         rewrite /= freeable_sz_full_S. iFrame. iExists (_::_::_).
         rewrite 2!heap_mapsto_vec_cons shift_loc_assoc uninit_own. iFrame.
         iIntros "!>!%". simpl. congruence. }
@@ -435,7 +435,7 @@ Section code.
       iMod ("Hclose" with "Hlw") as "Hna".
       iApply (type_type _ _ _ [ w ◁ box (uninit 1) ]
         with "[] LFT HE Hna HL Hk [-]"); last first.
-      { unlock. by rewrite tctx_interp_singleton tctx_hasty_val. }
+      { by rewrite tctx_interp_singleton tctx_hasty_val. }
       iApply type_jump; solve_typing.
   Qed.
 
diff --git a/theories/typing/lib/take_mut.v b/theories/typing/lib/take_mut.v
index aae1d7b7f5b1575db54e6032e4d9f975c83cd1a5..eff1c149c367bc64350ed8719872fd47f522348b 100644
--- a/theories/typing/lib/take_mut.v
+++ b/theories/typing/lib/take_mut.v
@@ -31,7 +31,7 @@ Section code.
     iApply (type_new ty.(ty_size)); [solve_typing..|]; iIntros (t); simpl_subst.
     (* Switch to Iris. *)
     iIntros (tid) "#LFT #HE Hna HL Hk (Ht & Hf' & Hx & Hx' & Henv & _)".
-    rewrite !tctx_hasty_val [[x]]lock [[f']]lock [[env]]lock.
+    rewrite !tctx_hasty_val /=.
     iDestruct (ownptr_uninit_own with "Ht") as (tl tvl) "(% & >Htl & Htl†)". subst t. simpl.
     destruct x' as [[|lx'|]|]; try done. simpl.
     iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose1)"; [solve_typing..|].
@@ -55,12 +55,12 @@ Section code.
         [k ◁cont(_, λ x:vec val 1, [ x!!!0 ◁ box ty])]
         [ f' ◁ fn(∅; envty, ty) → ty; #tl ◁ box ty; env ◁ box envty ]
        with "[] LFT [] Hna [Hβ Hβ†] [-Hf' Htl Htl† Hx'vl Henv]"); swap 1 3; swap 4 5.
-    { rewrite /llctx_interp. iSplitL; last done. (* FIXME: iSplit should work as one side is 'True', thus persistent. *)
+    { rewrite /llctx_interp /=. iSplit; last done.
       iExists β. simpl. iSplit; first by rewrite left_id. iFrame "∗#". }
     { iSplitL; last iApply "HE". iExact "Hβϝ". }
     { iApply (type_call ()); solve_typing. (* This is showing that the lifetime bounds of f' are satisfied. *) }
     { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
-      unlock. iFrame. iExists _. iFrame. }
+      iFrame. iExists _. iFrame. }
     (* Prove the continuation of the function call. *)
     iIntros (? ->%elem_of_list_singleton arg) "Hna Hβ". inv_vec arg=>r.
     iIntros "[Hr _]". rewrite tctx_hasty_val /=.
@@ -81,7 +81,7 @@ Section code.
     iApply (type_type _ _ _ [ x ◁ _; #lr ◁ box (uninit ty.(ty_size)) ]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
-      unlock. iFrame. iExists _. rewrite uninit_own. iFrame. auto using vec_to_list_length. }
+      iFrame. iExists _. rewrite uninit_own. iFrame. auto using vec_to_list_length. }
     iApply type_delete; [solve_typing..|].
     iApply type_delete; [solve_typing..|].
     iApply (type_new _); [solve_typing..|]; iIntros (r); simpl_subst.