diff --git a/_CoqProject b/_CoqProject
index a8156fdf6a0096eb5bdaad53dd2800d5e9c5e314..1cd9e93ada52e25e0b3421c75f9b8bc62056a450 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -19,6 +19,7 @@ theories/lang/notation.v
 theories/lang/memcpy.v
 theories/lang/new_delete.v
 theories/lang/swap.v
+theories/lang/lock.v
 theories/typing/base.v
 theories/typing/lft_contexts.v
 theories/typing/type.v
diff --git a/opam b/opam
index 1f4a25a2efb009bb5b2112212009739ffbce71f4..76e3aa8b5c1696a24c752540d5c393600fe2f481 100644
--- a/opam
+++ b/opam
@@ -10,5 +10,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-gpfsl" { (= "dev.2018-05-23.5.2f8996b5") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2018-05-24.1.c64c8c9a") | (= "dev") }
 ]
diff --git a/theories/lang/lock.v b/theories/lang/lock.v
index cf2c520e02265bbf097bbbd3ee62c03b470e8ff2..403a4623d84064bbd8ed3f6abb525f234d2eac69 100644
--- a/theories/lang/lock.v
+++ b/theories/lang/lock.v
@@ -43,6 +43,8 @@ Section proof.
   Global Instance lock_proto_inv_ne l γ: NonExpansive (lock_proto_inv l γ).
   Proof. rewrite /lock_proto_inv =>????. apply GPS_PPInv_ne. solve_proper. Qed.
 
+  Global Instance lock_proto_lc_persistent: Persistent (lock_proto_lc l γ R0 R) := _.
+
   Lemma lock_proto_lc_iff l γ R0 R R' :
     □ (R ↔ R') -∗ lock_proto_lc l γ R0 R -∗ lock_proto_lc l γ R0 R'.
   Proof.
@@ -74,43 +76,43 @@ Section proof.
   Proof. by iIntros "#$". Qed.
 
   (** The main proofs. *)
-  Lemma lock_proto_create (R : vProp) l (b : bool) : 
-    l ↦ #b -∗ (if b then True else ▷ R) ==∗
-      ∃ γ, lock_proto_lc l γ R R ∗ ▷ lock_proto_inv l γ R.
+  Lemma lock_proto_create (R : vProp) l (b bl : bool) :
+    l ↦ #b -∗ (if b then True else ▷?bl R) ==∗
+      ∃ γ, lock_proto_lc l γ R R ∗ ▷?bl lock_proto_inv l γ R.
   Proof.
     iIntros "Hl R".
-    iMod (GPS_PPRaw_Init_vs (lock_interp R) _ _ () with "Hl [R] []")
+    iMod (GPS_PPRaw_Init_vs (lock_interp R) _ bl _ () with "Hl [R] []")
       as (γ) "[lc inv]".
     { rewrite /lock_interp. iExists b. iSplit; [done|]. by destruct b. }
     { rewrite /lock_interp. by iExists b. }
     iExists γ. iFrame "lc inv". iIntros "!> !#". by iApply (bi.iff_refl True%I).
   Qed.
 
-  Lemma lock_proto_destroy l jγ R E (SUB: ↑histN ⊆ E) :
-    ⎡ hist_inv ⎤ -∗ lock_proto_inv l jγ R
-    ={E}=∗ ∃ (b : bool), l ↦ #b ∗ if b then True else R.
+  Lemma lock_proto_destroy bl l jγ R E (SUB: ↑histN ⊆ E) :
+    ⎡ hist_inv ⎤ -∗ ▷?bl lock_proto_inv l jγ R
+    ={E}=∗ ∃ (b : bool), l ↦ #b ∗ if b then True else ▷?bl R.
   Proof.
     iIntros "#hInv inv".
     iMod (GPS_PPInv_dealloc with "hInv inv") as (s v) "(Hl & F & _)"; [done|].
-    iDestruct "F" as (b) "[% R]". subst v. iExists b. by iFrame "Hl R".
+    iDestruct "F" as (b) "[>% R]". subst v. iExists b. iFrame "Hl". by destruct b.
   Qed.
 
-  Lemma mklock_unlocked_spec l R tid E :
+  Lemma mklock_unlocked_spec b l R tid E :
     ↑histN ⊆ E →
-    {{{ l ↦ ? ∗ ▷ R }}}
+    {{{ l ↦ ? ∗ ▷?b R }}}
       mklock_unlocked [ #l ] in tid @ E
-    {{{ γ, RET #☠; lock_proto_lc l γ R R ∗ ▷ lock_proto_inv l γ R }}}.
+    {{{ γ, RET #☠; lock_proto_lc l γ R R ∗ ▷?b lock_proto_inv l γ R }}}.
   Proof.
     iIntros (? Φ) "[Hl HR] HΦ". wp_lam. rewrite -wp_fupd. wp_write.
-    iMod (lock_proto_create R _ false with "Hl [$HR]") as (γ) "?".
+    iMod (lock_proto_create R _ false b with "Hl [$HR]") as (γ) "?".
     by iApply "HΦ".
   Qed.
 
-  Lemma mklock_locked_spec l R tid E :
+  Lemma mklock_locked_spec b l R tid E :
     ↑histN ⊆ E →
     {{{ l ↦ ? }}}
       mklock_locked [ #l ] in tid @ E
-    {{{ γ, RET #☠; lock_proto_lc l γ R R ∗ ▷ lock_proto_inv l γ R }}}.
+    {{{ γ, RET #☠; lock_proto_lc l γ R R ∗ ▷?b lock_proto_inv l γ R }}}.
   Proof.
     iIntros (? Φ) "Hl HΦ". wp_lam. rewrite -wp_fupd. wp_write.
     iMod (lock_proto_create R _ true with "Hl [//]") as (γ) "?".
@@ -125,7 +127,7 @@ Section proof.
                   ∗ (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 R0 else True) ∗ P }}}.
+    {{{ 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)".
@@ -146,7 +148,7 @@ Section proof.
     iNext. iIntros (b v' s') "(_ & inv & _ & CASE)"; simpl.
     iMod ("Hclose" with "inv") as "P".
     iModIntro. iApply "HΦ". iFrame "P".
-    iDestruct "CASE" as "[[[% _] ?]|[[% _]_]]"; by subst b.
+    iDestruct "CASE" as "[[[% _] ?]|[[% _]_]]"; subst b; [by iApply "Eq"|done].
   Qed.
 
   Lemma acquire_spec l (R0 R P: vProp) tid E1 E2 :
@@ -154,7 +156,7 @@ Section proof.
     □ (P ={E2,E1}=∗ ∃ γ 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 #☠; R0 ∗ P }}}.
+    {{{ P }}} acquire [ #l ] in tid @ E2 {{{ RET #☠; R ∗ P }}}.
   Proof.
     iIntros (??) "#Hproto !# * HP HΦ". iLöb as "IH". wp_rec.
     wp_apply (try_acquire_spec with "Hproto HP"); [done..|by etrans|].
@@ -168,14 +170,15 @@ Section proof.
     □ (P ={E2,E1}=∗ ∃ γ 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)) -∗
-    {{{ R0 ∗ P }}} release [ #l ] in tid @ E2 {{{ RET #☠; 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)".
     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 "_ !>".
-      iSplitL "HR"; iExists false; [by iFrame "HR"|done]. }
+      iSplitL "HR"; iExists false; [|done].
+      iSplit; [done|by iApply "Eq"]. }
     iNext. iIntros "[? inv]". iMod ("Hclose" with "inv"). by iApply "HΦ".
   Qed.
 End proof.
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
new file mode 100644
index 0000000000000000000000000000000000000000..ef2edf92701205978dc340233783ca69bc0d5939
--- /dev/null
+++ b/theories/typing/lib/mutex/mutex.v
@@ -0,0 +1,253 @@
+From Coq.QArith Require Import Qcanon.
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import auth csum frac agree.
+From iris.bi Require Import big_op.
+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 option.
+Set Default Proof Using "Type".
+
+Definition mutexN := lrustN .@ "mutex".
+
+Section mutex.
+  Context `{!typeG Σ, lockG Σ}.
+
+  (*
+    pub struct Mutex<T: ?Sized> {
+      // Note that this mutex is in a *box*, not inlined into the struct itself.
+      // Once a native mutex has been used once, its address can never change (it
+      // can't be moved). This mutex type can be safely moved at any time, so to
+      // ensure that the native mutex is used correctly we box the inner lock to
+      // give it a constant address.
+      inner: Box<sys::Mutex>,
+      poison: poison::Flag,
+      data: UnsafeCell<T>,
+    }
+  *)
+
+  Program Definition mutex (ty : type) :=
+    {| ty_size := 1 + ty.(ty_size);
+       ty_own tid vl :=
+        ⎡hist_inv⎤ ∗ match vl return _ with
+         | #(LitInt z) :: vl' =>
+           ⌜∃ b, z = Z_of_bool b⌝ ∗ ty.(ty_own) tid vl'
+         | _ => False end;
+       ty_shr κ tid l := ∃ κ', κ ⊑ κ' ∗
+        ∃ γ R, lock_proto_lc l γ R (&{κ'}((l >> 1) ↦∗: ty.(ty_own) tid))
+                ∗ &at{κ, mutexN} (lock_proto_inv l γ R)
+    |}%I.
+  Next Obligation.
+    iIntros (??[|[[]|]]); try iIntros "[? []]". rewrite ty_size_eq.
+    iIntros "[_ [_ %]] !% /=". congruence.
+  Qed.
+  Next Obligation.
+    iIntros (ty E κ l tid q ?) "#LFT Hbor Htok".
+    iMod (bor_acc_cons with "LFT Hbor Htok") as "[H Hclose]"; first done.
+    iDestruct "H" as ([|[[| |n]|]vl]) "[H↦ [#hInv H]]"; try iDestruct "H" as ">[]".
+    rewrite own_loc_na_vec_cons. iDestruct "H↦" as ">[Hl H↦]".
+    iDestruct "H" as "[>EQ Hown]". iDestruct "EQ" as %[b ->].
+    (* We need to turn the ohne borrow into two, so we close it -- and then
+       we open one of them again. *)
+    iMod ("Hclose" $! ((∃ b, l ↦ #(Z_of_bool b)) ∗ ((l >> 1) ↦∗: ty_own ty tid))%I
+          with "[] [Hl H↦ Hown]") as "[Hbor Htok]".
+    { clear. iNext. iIntros "[Hl Hown] !>". iNext. iDestruct "Hl" as (b) "Hl".
+      iDestruct "Hown" as (vl) "[H↦ Hown]". iExists (#(Z_of_bool b) :: vl).
+      rewrite own_loc_na_vec_cons. iFrame "∗ hInv". iPureIntro. eauto. }
+    { iNext. iSplitL "Hl"; first by eauto.
+      iExists vl. iFrame. }
+    clear b vl. iMod (bor_sep with "LFT Hbor") as "[Hl Hbor]"; first done.
+    iMod (bor_acc_cons with "LFT Hl Htok") as "[>Hl Hclose]"; first done.
+    iDestruct "Hl" as (b) "Hl".
+    iMod (lock_proto_create _ _ _ false with "Hl [Hbor]") as (γ) "[Hlc Hproto]".
+    { destruct b; [done|by iExact "Hbor"]. }
+    iMod ("Hclose" with "[] Hproto") as "[Hl Htok]".
+    { clear b. iIntros "!> Hproto". simpl.
+      iMod (lock_proto_destroy true with "hInv Hproto") as (b) "[Hl _]"; [done|].
+      iExists _. by iFrame. }
+    iFrame "Htok". iExists κ.
+    iMod (bor_share mutexN with "Hl") as "Hl"; [solve_ndisj..|].
+    iSplitL ""; [iApply lft_incl_refl|]. iExists γ, _. by iFrame.
+  Qed.
+  Next Obligation.
+    iIntros (ty κ κ' tid l) "#Hincl H".
+    iDestruct "H" as (κ'') "(#Hlft & #Hlck)".
+    iDestruct "Hlck" as (γ R) "[Hlc Hproto]".
+    iExists _. iSplit; [by iApply lft_incl_trans|].
+    iExists _, _. iFrame "Hlc". by iApply at_bor_shorten.
+  Qed.
+
+  Global Instance mutex_wf ty `{!TyWf ty} : TyWf (mutex ty) :=
+    { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+
+  (* Global Instance mutex_type_ne : TypeNonExpansive mutex.
+  Proof.
+    constructor;
+      solve_proper_core ltac:(fun _ => exact: type_dist2_S ||
+                                              f_type_equiv || f_contractive || f_equiv).
+  Qed. *)
+
+  (* Global Instance mutex_ne : NonExpansive mutex.
+  Proof.
+    constructor; solve_proper_core ltac:(fun _ => (eapply ty_size_ne; try reflexivity) || f_equiv).
+  Qed. *)
+
+  Global Instance mutex_mono E L : Proper (eqtype E L ==> subtype E L) mutex.
+  Proof.
+    move=>ty1 ty2 /eqtype_unfold EQ. iIntros (?) "HL".
+    iDestruct (EQ with "HL") as "#EQ". iIntros "!# #HE". clear EQ.
+    iDestruct ("EQ" with "HE") as "(% & #Howni & _) {EQ}".
+    iSplit; last iSplit.
+    - simpl. iPureIntro. f_equiv. done.
+    - iIntros "!# * Hvl". destruct vl as [|[[| |n]|]vl]; try done.
+      simpl. iDestruct "Hvl" as "[$ [$ Hvl]]". by iApply "Howni".
+    - iIntros "!# * Hshr". iDestruct "Hshr" as (κ') "[Hincl Hshr]".
+      iExists _. iFrame "Hincl". iDestruct "Hshr" as (γ R) "[Hlc Hbor]".
+      iExists γ, R. iFrame "Hbor".
+      iApply lock_proto_lc_iff_proper; [|iFrame].
+      iApply bor_iff_proper. iApply own_loc_na_pred_iff_proper.
+      iNext. iAlways; iIntros; iSplit; iIntros; by iApply "Howni".
+  Qed.
+
+  Global Instance mutex_proper E L :
+    Proper (eqtype E L ==> eqtype E L) mutex.
+  Proof. by split; apply mutex_mono. Qed.
+
+  Global Instance mutex_send ty :
+    Send ty → Send (mutex ty).
+  Proof.
+    iIntros (??? [|[[| |n]|]vl]); try done. iIntros "[$ [$ Hvl]]".
+    by iApply send_change_tid.
+  Qed.
+
+  Global Instance mutex_sync ty :
+    Send ty → Sync (mutex ty).
+  Proof.
+    iIntros (???? l) "Hshr". iDestruct "Hshr" as (κ') "[Hincl Hshr]".
+    iExists _. iFrame "Hincl". iDestruct "Hshr" as (γ R) "[Hlc Hbor]".
+    iExists γ, R. iFrame "Hbor".
+    iApply lock_proto_lc_iff_proper; [|iFrame].
+    iApply bor_iff_proper. iApply own_loc_na_pred_iff_proper.
+    iNext. iAlways; iIntros; iSplit; iIntros; by iApply send_change_tid.
+  Qed.
+End mutex.
+
+Section code.
+  Context `{!typeG Σ}.
+
+  Definition mutex_new ty : val :=
+    funrec: <> ["x"] :=
+      let: "m" := new [ #(mutex ty).(ty_size) ] in
+      "m" +ₗ #1 <-{ty.(ty_size)} !"x";;
+      mklock_unlocked ["m" +ₗ #0];;
+      delete [ #ty.(ty_size); "x"];; return: ["m"].
+
+  Lemma mutex_new_type ty `{!TyWf ty} :
+    typed_val (mutex_new ty) (fn(∅; ty) → mutex ty).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (_ ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    (* FIXME: It should be possible to infer the `S ty.(ty_size)` here.
+       This should be done in the @eq external hints added in lft_contexts.v. *)
+    iApply (type_new (S ty.(ty_size))); [solve_typing..|]; iIntros (m); simpl_subst.
+    (* FIXME: The following should work.  We could then go into Iris later.
+    iApply (type_memcpy ty); [solve_typing..|]. *)
+    (* Switch to Iris. *)
+    iIntros (tid) "#LFT #HE Hna HL Hk [Hm [Hx _]]".
+    rewrite !tctx_hasty_val /=.
+    iDestruct (ownptr_uninit_own with "Hm") as (lm vlm) "(% & Hm & Hm†)".
+    subst m. inv_vec vlm=>m vlm. simpl. iDestruct (heap_mapsto_vec_cons with "Hm") as "[Hm0 Hm]".
+    destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
+    iDestruct (heap_mapsto_ty_own with "Hx") as (vl) "[>Hx Hxown]".
+    (* All right, we are done preparing our context. Let's get going. *)
+    wp_op. wp_apply (wp_memcpy with "[$Hm $Hx]"); [by rewrite vec_to_list_length..|].
+    iIntros "[Hm Hx]". wp_seq. wp_op. rewrite shift_loc_0. wp_lam.
+    wp_write.
+    (* Switch back to typing mode. *)
+    iApply (type_type _ _ _ [ #lx ◁ box (uninit ty.(ty_size)); #lm ◁ box (mutex 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' //.
+      iFrame. iSplitL "Hx".
+      - iExists _. iFrame. by rewrite uninit_own vec_to_list_length.
+      - iExists (#false :: vl). rewrite heap_mapsto_vec_cons. iFrame; eauto. }
+    iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+
+  Definition mutex_into_inner ty : val :=
+    funrec: <> ["m"] :=
+      let: "x" := new [ #ty.(ty_size) ] in
+      "x" <-{ty.(ty_size)} !("m" +ₗ #1);;
+      delete [ #(mutex ty).(ty_size); "m"];; return: ["x"].
+
+  Lemma mutex_into_inner_type ty `{!TyWf ty} :
+    typed_val (mutex_into_inner ty) (fn(∅; mutex ty) → ty).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (_ ϝ ret arg). inv_vec arg=>m. simpl_subst.
+    iApply (type_new ty.(ty_size)); [solve_typing..|]; iIntros (x); simpl_subst.
+    (* Switch to Iris. *)
+    iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hm _]]".
+    rewrite !tctx_hasty_val /=.
+    iDestruct (ownptr_uninit_own with "Hx") as (lx vlx) "(% & Hx & Hx†)".
+    subst x. simpl.
+    destruct m as [[|lm|]|]; try done. iDestruct "Hm" as "[Hm Hm†]".
+    iDestruct (heap_mapsto_ty_own with "Hm") as (vlm) "[>Hm Hvlm]".
+    inv_vec vlm=>m vlm. destruct m as [[|m|]|]; try by iDestruct "Hvlm" as ">[]".
+    simpl. iDestruct (heap_mapsto_vec_cons with "Hm") as "[Hm0 Hm]".
+    iDestruct "Hvlm" as "[_ Hvlm]".
+    (* All right, we are done preparing our context. Let's get going. *)
+    wp_op. wp_apply (wp_memcpy with "[$Hx $Hm]"); [by rewrite vec_to_list_length..|].
+    (* FIXME: Swapping the order of $Hx and $Hm breaks. *)
+    iIntros "[Hx Hm]". wp_seq.
+    (* Switch back to typing mode. *)
+    iApply (type_type _ _ _ [ #lx ◁ box ty; #lm ◁ box (uninit (mutex ty).(ty_size))]
+        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' //.
+      iFrame. iSplitR "Hm0 Hm".
+      - iExists _. iFrame.
+      - iExists (_ :: _). rewrite heap_mapsto_vec_cons. iFrame.
+        rewrite uninit_own. rewrite /= vec_to_list_length. eauto. }
+    iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+
+  Definition mutex_get_mut : val :=
+    funrec: <> ["m"] :=
+      let: "m'" := !"m" in
+      "m" <- ("m'" +ₗ #1);;
+      return: ["m"].
+
+  Lemma mutex_get_mut_type ty `{!TyWf ty} :
+    typed_val mutex_get_mut (fn(∀ α, ∅; &uniq{α}(mutex ty)) → &uniq{α} ty).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ϝ ret arg); inv_vec arg=>m; simpl_subst.
+    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.
+    destruct m' as [[|lm'|]|]; try done. simpl.
+    iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose1)";
+      [solve_typing..|].
+    iMod (bor_acc_cons with "LFT Hm' Hα") as "[Hm' Hclose2]"; first done.
+    wp_op. iDestruct "Hm'" as (vl) "[H↦ Hm']".
+    destruct vl as [|[[|m'|]|] vl]; try done. simpl.
+    iDestruct (heap_mapsto_vec_cons with "H↦") as "[H↦1 H↦2]".
+    iDestruct "Hm'" as "[% Hvl]".
+    iMod ("Hclose2" $! ((lm' +ₗ 1) ↦∗: ty_own ty tid)%I with "[H↦1] [H↦2 Hvl]") as "[Hbor Hα]".
+    { iIntros "!> Hlm' !>". iNext. clear vl. iDestruct "Hlm'" as (vl) "[H↦ Hlm']".
+      iExists (_ :: _). rewrite heap_mapsto_vec_cons. do 2 iFrame. done. }
+    { iExists vl. iFrame. }
+    iMod ("Hclose1" with "Hα HL") as "HL".
+    (* Switch back to typing mode. *)
+    iApply (type_type _ _ _ [ m ◁ 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 type_assign; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+End code.
\ No newline at end of file