diff --git a/_CoqProject b/_CoqProject
index f024e4d30d185f8d78d2cb62f61de44efb6956df..6c77eaa1639c49d6833ba72479d159b7f81c4ec8 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -53,6 +53,7 @@ theories/typing/lib/take_mut.v
 theories/typing/lib/rc/rc.v
 theories/typing/lib/rc/weak.v
 theories/typing/lib/mutex/mutex.v
+theories/typing/lib/mutex/mutexguard.v
 theories/typing/lib/refcell/refcell_code.v
 theories/typing/lib/refcell/refcell.v
 theories/typing/lib/refcell/ref_code.v
diff --git a/theories/lang/lock.v b/theories/lang/lock.v
index 43e925120fab8db84b4ce5fdb19d68322ea7f847..356188fdaaa1486de6b98d924a25926c36ac50f2 100644
--- a/theories/lang/lock.v
+++ b/theories/lang/lock.v
@@ -123,16 +123,16 @@ Section proof.
 
   (* At this point, it'd be really nice to have some sugar for symmetric
      accessors. *)
-  Lemma try_acquire_spec l (R0 R P: vProp) tid E1 E2 :
+  Lemma try_acquire_spec l (R P: vProp) tid E1 E2 :
     ↑histN ⊆ E1 → E1 ⊆ E2 →
-    □ (P ={E2,E1}=∗ ∃ γ Vb, lock_proto_lc l γ R0 R
+    □ (P ={E2,E1}=∗ ∃ γ R0 Vb, lock_proto_lc l γ R0 R
                   ∗ (monPred_in Vb → ▷ lock_proto_inv l γ R0)
                   ∗ ((monPred_in Vb → ▷ lock_proto_inv l γ R0) ={E1,E2}=∗ P)) -∗
     {{{ P }}} try_acquire [ #l ] in tid @ E2
     {{{ b, RET #b; (if b is true then R else True) ∗ P }}}.
   Proof.
     iIntros (??) "#Hproto !# * HP HΦ".
-    wp_rec. iMod ("Hproto" with "HP") as (γ Vb) "(#[Eq lc] & inv & Hclose)".
+    wp_rec. iMod ("Hproto" with "HP") as (γ R0 Vb) "(#[Eq lc] & inv & Hclose)".
     iMod (rel_True_intro True%I tid with "[//]") as "rTrue".
     iApply (GPS_PPRaw_CAS_simple (lock_interp R0) _ _ _
                 (Z_of_bool false) #true () (λ _, R0)%I (λ _ _, True)%I
@@ -153,9 +153,9 @@ Section proof.
     iDestruct "CASE" as "[[[% _] ?]|[[% _]_]]"; subst b; [by iApply "Eq"|done].
   Qed.
 
-  Lemma acquire_spec l (R0 R P: vProp) tid E1 E2 :
+  Lemma acquire_spec l (R P: vProp) tid E1 E2 :
     ↑histN ⊆ E1 → E1 ⊆ E2 →
-    □ (P ={E2,E1}=∗ ∃ γ Vb, lock_proto_lc l γ R0 R
+    □ (P ={E2,E1}=∗ ∃ γ R0 Vb, lock_proto_lc l γ R0 R
                   ∗ (monPred_in Vb → ▷ lock_proto_inv l γ R0)
                   ∗ ((monPred_in Vb → ▷ lock_proto_inv l γ R0) ={E1,E2}=∗ P)) -∗
     {{{ P }}} acquire [ #l ] in tid @ E2 {{{ RET #☠; R ∗ P }}}.
@@ -167,15 +167,15 @@ Section proof.
     - iIntros "[_ Hown]". wp_if. iApply ("IH" with "Hown HΦ").
   Qed.
 
-  Lemma release_spec l (R0 R P: vProp) tid E1 E2 :
+  Lemma release_spec l (R P: vProp) tid E1 E2 :
     ↑histN ⊆ E1 → E1 ⊆ E2 →
-    □ (P ={E2,E1}=∗ ∃ γ Vb, lock_proto_lc l γ R0 R
+    □ (P ={E2,E1}=∗ ∃ γ R0 Vb, lock_proto_lc l γ R0 R
                   ∗ (monPred_in Vb → ▷ lock_proto_inv l γ R0)
                   ∗ ((monPred_in Vb → ▷ lock_proto_inv l γ R0) ={E1,E2}=∗ P)) -∗
     {{{ R ∗ P }}} release [ #l ] in tid @ E2 {{{ RET #☠; P }}}.
   Proof.
     iIntros (??) "#Hproto !# * (HR & HP) HΦ". wp_let.
-    iMod ("Hproto" with "HP") as (γ Vb) "(#[Eq lc] & inv & Hclose)".
+    iMod ("Hproto" with "HP") as (γ R0 Vb) "(#[Eq lc] & inv & Hclose)".
     iApply (GPS_PPRaw_write (lock_interp R0) _ _ #(Z_of_bool false) _ ()
             with "[$lc $inv HR]"); [by move => []|done|by right|..].
     { rewrite /lock_interp /=. iNext. iIntros "_ !>".
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
new file mode 100644
index 0000000000000000000000000000000000000000..d5921ea2e897bddde93c334a17b1b9a4b8f6aea8
--- /dev/null
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -0,0 +1,318 @@
+From Coq.QArith Require Import Qcanon.
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import frac.
+From lrust.lang Require Import memcpy lock.
+From lrust.lifetime Require Import at_borrow.
+From lrust.typing Require Export type.
+From lrust.typing Require Import typing util option mutex.
+Set Default Proof Using "Type".
+
+(* This type is an experiment in defining a Rust type on top of a non-typesysten-specific
+   interface, like the one provided by lang.lock.
+   It turns out that we need an accessor-based spec for this purpose, so that
+   we can put the protocol into shared borrows.  Cancellable invariants
+   don't work because their cancelling view shift has a non-empty mask,
+   and it would have to be executed in the consequence view shift of
+   a borrow.
+*)
+
+Section mguard.
+  Context `{!typeG Σ, !lockG Σ}.
+
+  (*
+    pub struct MutexGuard<'a, T: ?Sized + 'a> {
+      // funny underscores due to how Deref/DerefMut currently work (they
+      // disregard field privacy).
+      __lock: &'a Mutex<T>,
+      __poison: poison::Guard,
+    }
+  *)
+
+  Program Definition mutexguard (α : lft) (ty : type) :=
+    {| ty_size := 1;
+       ty_own tid vl :=
+         match vl return _ with
+         | [ #(LitLoc l) ] =>
+           ∃ β, α ⊑ β ∗
+             (∃ γ R, lock_proto_lc l γ R (&{β} ((l >> 1) ↦∗: ty.(ty_own) tid))
+              ∗ &at{α, mutexN} (lock_proto_inv l γ R))
+             ∗ &{β} ((l >> 1) ↦∗: ty.(ty_own) tid)
+         | _ => False end;
+       ty_shr κ tid l :=
+         ∃ (l':loc), &frac{κ}(λ q', l ↦{q'} #l') ∗
+            □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[α⊓κ]
+                ={F, F∖↑shrN}▷=∗ ty.(ty_shr) (α⊓κ) tid (l' >> 1) ∗ q.[α⊓κ]
+    |}%I.
+  Next Obligation. by iIntros (? ty tid [|[[]|][]]) "H". Qed.
+  (* This is to a large extend copy-pasted from RWLock's write guard. *)
+  Next Obligation.
+    iIntros (α ty E κ l tid q HE) "#LFT Hb Htok".
+    iMod (bor_exists with "LFT Hb") as (vl) "Hb"; first done.
+    iMod (bor_sep with "LFT Hb") as "[H↦ Hb]"; first done.
+    iMod (bor_fracture _ (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦"; [done|].
+    destruct vl as [|[[|l'|]|][]];
+      try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
+    setoid_rewrite own_loc_na_vec_singleton.
+    iMod (bor_exists with "LFT Hb") as (β) "Hb"; first done.
+    iMod (bor_sep with "LFT Hb") as "[Hαβ H]"; first done.
+    iMod (bor_sep with "LFT H") as "[_ H]"; first done.
+    iMod (bor_persistent with "LFT Hαβ Htok") as "[#Hαβ $]"; first done.
+    iExists _. iFrame "H↦". iApply delay_sharing_nested; try done.
+    (* FIXME: "iApply lft_intersect_mono" only preserves the later on the last
+       goal, as does "iApply (lft_intersect_mono with ">")". *)
+    iNext. iApply lft_intersect_mono. done. iApply lft_incl_refl.
+  Qed.
+  Next Obligation.
+    iIntros (??????) "#? H". iDestruct "H" as (l') "[#Hf #H]".
+    iExists _. iSplit.
+    - by iApply frac_bor_shorten.
+    - iIntros "!# * % Htok".
+      iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
+      { iApply lft_intersect_mono. iApply lft_incl_refl. done. }
+      iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
+      iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
+      iApply ty_shr_mono; try done. iApply lft_intersect_mono. iApply lft_incl_refl. done.
+  Qed.
+
+  Global Instance mutexguard_wf α ty `{!TyWf ty} : TyWf (mutexguard α ty) :=
+    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) α }.
+
+  Global Instance mutexguard_type_contractive α : TypeContractive (mutexguard α).
+  Proof.
+    constructor;
+      solve_proper_core ltac:(fun _ => f_type_equiv || f_contractive || f_equiv
+                                    || exact: type_dist2_S).
+  Qed.
+  Global Instance mutexguard_ne α : NonExpansive (mutexguard α).
+  Proof. apply type_contractive_ne, _. Qed.
+
+  Global Instance mutexguard_mono E L :
+    Proper (flip (lctx_lft_incl E L) ==> eqtype E L ==> subtype E L) mutexguard.
+  Proof.
+    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].
+    - iIntros (tid [|[[]|][]]) "H"; try done. simpl.
+      iDestruct "H" as (β) "(#H⊑ & Hinv & Hown)".
+      iExists β. iFrame. iSplit; last iSplit.
+      + by iApply lft_incl_trans.
+      + iDestruct "Hinv" as (γ R) "[Hlc Hinv]".
+        iExists γ, R. iSplitL "Hlc".
+        * iApply lock_proto_lc_iff_proper; [|iFrame].
+          iApply bor_iff_proper. iNext. iApply own_loc_na_pred_iff_proper.
+          iAlways; iIntros; iSplit; iIntros; by iApply "Ho".
+        * iApply (at_bor_shorten with "Hα").
+          iApply (at_bor_iff with "[] Hinv"). iIntros "!> !#".
+          by iApply (bi.iff_refl True%I).
+      + iApply bor_iff; last done. iIntros "!>".
+        iApply own_loc_na_pred_iff_proper.
+        iAlways; 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.
+      { iApply lft_intersect_mono. done. iApply lft_incl_refl. }
+      iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
+      iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
+      iApply ty_shr_mono; try done. iApply lft_intersect_mono. done. iApply lft_incl_refl.
+      by iApply "Hs".
+  Qed.
+
+  Global Instance mutexguard_proper E L :
+    Proper (lctx_lft_eq E L ==> eqtype E L ==> eqtype E  L) mutexguard.
+  Proof. intros ??[]???. split; by apply mutexguard_mono. Qed.
+
+  Global Instance mutexguard_sync α ty :
+    Sync ty → Sync (mutexguard α ty).
+  Proof.
+    move=>?????/=. apply bi.exist_mono=>?. do 6 f_equiv.
+    by rewrite sync_change_tid.
+  Qed.
+
+  (* POSIX requires the unlock to occur from the thread that acquired
+     the lock, so Rust does not implement Send for RwLockWriteGuard. We could
+     prove this. *)
+End mguard.
+
+Section code.
+  Context `{!typeG Σ, !lockG Σ}.
+
+  Lemma mutex_acc E l ty tid q α κ :
+    ↑histN ⊆ E → ↑lftN ⊆ E → ↑mutexN ⊆ E →
+    let R := (&{κ}((l >> 1) ↦∗: ty_own ty tid))%I in
+    ⎡ lft_ctx ⎤ -∗
+    (∃ γ R0, lock_proto_lc l γ R0 R
+              ∗ &at{α, mutexN} (lock_proto_inv l γ R0))%I -∗
+    α ⊑ κ -∗
+    □ ((q).[α] ={E,↑histN}=∗
+            ∃ γ R0 Vb, lock_proto_lc l γ R0 R
+                  ∗ (monPred_in Vb → ▷ lock_proto_inv l γ R0)
+                  ∗ ((monPred_in Vb → ▷ lock_proto_inv l γ R0) ={↑histN,E}=∗ (q).[α]))%I.
+  Proof.
+    iIntros (??? R) "#LFT #Hshr #Hlincl !# Htok".
+    iDestruct "Hshr" as (γ R0) "[Hlc Hshr]". iExists γ, R0.
+    iMod (at_bor_acc with "LFT Hshr Htok") as (Vb) "[Hproto Hclose1]"; [done..|].
+    iExists Vb. iFrame "Hlc Hproto".
+    iMod (fupd_intro_mask') as "Hclose2"; last iModIntro; first solve_ndisj.
+    iIntros "Hproto". iMod "Hclose2" as "_".
+    iMod ("Hclose1" with "Hproto") as "$". done.
+  Qed.
+
+  Definition mutex_lock : val :=
+    funrec: <> ["mutex"] :=
+      let: "m" := !"mutex" in
+      let: "guard" := new [ #1 ] in
+      acquire ["m"];;
+      "guard" +ₗ #0 <- "m";;
+      delete [ #1; "mutex" ];; return: ["guard"].
+
+  Lemma mutex_lock_type ty `{!TyWf ty} :
+    typed_val mutex_lock (fn(∀ α, ∅; &shr{α}(mutex ty)) → mutexguard α ty).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    iApply type_deref; [solve_typing..|]; iIntros (m); simpl_subst.
+    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 /=.
+    destruct m as [[|lm|]|]; try done. iDestruct "Hm" as (κ') "[#Hακ' #Hshr]".
+    iDestruct (ownptr_uninit_own with "Hg") as (lg vlg) "(% & Hg & Hg†)".
+    subst g. inv_vec vlg=>g. rewrite own_loc_na_vec_singleton.
+    (* 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..|].
+    wp_apply (acquire_spec with "[] Hα");
+      [reflexivity|done|by iApply (mutex_acc with "LFT Hshr Hακ'")|..].
+    iIntros "[Hcont Htok]". wp_seq. wp_op. rewrite shift_0. wp_write.
+    iMod ("Hclose1" with "Htok HL") as "HL".
+    (* Switch back to typing mode. *)
+    iApply (type_type _ _ _ [ x ◁ own_ptr _ _; #lg ◁ box (mutexguard α ty)]
+        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 own_loc_na_vec_singleton. iFrame "Hg".
+      iExists _. iFrame "#∗". }
+    iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+
+  Definition mutexguard_derefmut : val :=
+    funrec: <> ["g"] :=
+      let: "g'" := !"g" in
+      let: "m" := !"g'" in
+      letalloc: "r" <- ("m" +ₗ #1) in
+      delete [ #1; "g"];; return: ["r"].
+
+  Lemma mutexguard_derefmut_type ty `{!TyWf ty} :
+    typed_val mutexguard_derefmut (fn (fun '(α, β) =>
+      FP_wf ∅ [# &uniq{α}(mutexguard β ty)]%T (&uniq{α}ty)%T)).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros ([α β] ϝ ret arg). inv_vec arg=>g. simpl_subst.
+    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 /=.
+    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.
+    iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose1)";
+      [solve_typing..|].
+    destruct vl as [|[[|lm|]|] [|]]; simpl;
+      try by iMod (bor_persistent with "LFT Hprot Hα") as "[>[] _]".
+    rewrite own_loc_na_vec_singleton.
+    iMod (bor_exists with "LFT Hprot") as (κ) "Hprot"; first done.
+    iMod (bor_sep with "LFT Hprot") as "[Hβκ Hprot]"; first done.
+    iMod (bor_sep with "LFT Hprot") as "[_ Hlm]"; first done.
+    iMod (bor_persistent with "LFT Hβκ Hα") as "[#Hβκ Hα]"; first done.
+    iMod (bor_acc with "LFT H↦ Hα") as "[H↦ Hclose2]"; first done.
+    wp_bind (!_)%E. iMod (bor_unnest with "LFT Hlm") as "Hlm"; first done.
+    wp_read. wp_let. iMod "Hlm".
+    iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
+    iMod ("Hclose2" with "H↦") as "[_ Hα]".
+    iMod ("Hclose1" with "Hα HL") as "HL".
+    (* Switch back to typing mode. *)
+    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.
+      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.
+    iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+
+  Definition mutexguard_deref : val := mutexguard_derefmut.
+
+  Lemma mutexguard_deref_type ty `{!TyWf ty} :
+    typed_val mutexguard_derefmut (fn (fun '(α, β) =>
+      FP_wf ∅ [# &shr{α}(mutexguard β ty)]%T (&shr{α}ty)%T)).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros ([α β] ϝ ret arg). inv_vec arg=>g. simpl_subst.
+    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 /=.
+    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)";
+      [solve_typing..|].
+    iMod (frac_bor_acc with "LFT Hlg Hα1") as (qlx') "[H↦ Hclose2]"; first done.
+    iMod (lctx_lft_alive_tok β with "HE HL") as (qβ) "(Hβ & HL & Hclose3)";
+      [solve_typing..|].
+    iDestruct (lft_intersect_acc with "Hβ Hα2") as (qβα) "[Hα2β Hclose4]".
+    wp_bind (!_)%E. iApply (wp_step_fupd with "[Hshr Hα2β]");
+         [done| |by iApply ("Hshr" with "[] Hα2β")|]; first done.
+    wp_read. iIntros "[#Hshr Hα2β] !>". wp_let.
+    iDestruct ("Hclose4" with "Hα2β") as "[Hβ Hα2]".
+    iMod ("Hclose3" with "Hβ HL") as "HL".
+    iMod ("Hclose2" with "H↦") as "Hα1".
+    iMod ("Hclose1" with "[$] HL") as "HL".
+    iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
+    (* Switch back to typing mode. *)
+    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.
+      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..|].
+    iApply type_jump; solve_typing.
+  Qed.
+
+  Definition mutexguard_drop : val :=
+    funrec: <> ["g"] :=
+      let: "m" := !"g" in
+      release ["m"];;
+      delete [ #1; "g" ];;
+      let: "r" := new [ #0 ] in return: ["r"].
+
+  Lemma mutexguard_drop_type ty `{!TyWf ty} :
+    typed_val mutexguard_drop (fn(∀ α, ∅; mutexguard α ty) → unit).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ϝ ret arg). inv_vec arg=>g. simpl_subst.
+    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 /=.
+    destruct m as [[|lm|]|]; try done. iDestruct "Hm" as (β) "(#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..|].
+    wp_apply (release_spec with "[] [Hα Hcnt]");
+      [reflexivity|done|by iApply (mutex_acc with "LFT Hshr Hαβ")|by iFrame|..].
+    iIntros "Htok". wp_seq. iMod ("Hclose1" with "Htok HL") as "HL".
+    (* 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. }
+    iApply type_delete; [solve_typing..|].
+    iApply type_new; [solve_typing..|]; iIntros (r); simpl_subst.
+    iApply type_jump; solve_typing.
+  Qed.
+
+  (* TODO: Should we do try_lock? *)
+  (* FIXME: When we have time, yeah! *)
+End code.