diff --git a/_CoqProject b/_CoqProject
index a98ee6e6611ef8966809ff79f2ae8dbc6604ff18..fa71794fd51678877147fdde972bc5f641626fe8 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -57,3 +57,4 @@ theories/typing/unsafe/refcell/ref.v
 theories/typing/unsafe/refcell/refmut.v
 theories/typing/unsafe/refcell/refcell_code.v
 theories/typing/unsafe/refcell/ref_code.v
+theories/typing/unsafe/refcell/refmut_code.v
diff --git a/theories/typing/unsafe/refcell/ref_code.v b/theories/typing/unsafe/refcell/ref_code.v
index 6430453e12a0c37d39b2d7f9e552261f856fa4c4..c373300da32e5cdf98f408aca4d3d10062461164 100644
--- a/theories/typing/unsafe/refcell/ref_code.v
+++ b/theories/typing/unsafe/refcell/ref_code.v
@@ -13,35 +13,33 @@ Section ref_functions.
   Lemma refcell_inv_reading_inv tid l γ α ty q ν :
     refcell_inv tid l γ α ty -∗
     own γ (◯ reading_st q ν) -∗
-    ∃ q' q'' n, l ↦ #(Zpos n) ∗
-            own γ (● Some (Cinr (to_agree ν, q', n)) ⋅ ◯ reading_st q ν) ∗
-            ⌜(q' + q'' = 1)%Qp ∧ (q ≤ q')%Qc⌝ ∗ q''.[ν] ∗
+    ∃ (q' : Qp) n, l ↦ #(Zpos n) ∗ ⌜(q ≤ q')%Qc⌝ ∗
+            own γ (● Some (to_agree ν, Cinr (q', n)) ⋅ ◯ reading_st q ν) ∗
             ty.(ty_shr) (α ∪ ν) tid (shift_loc l 1) ∗
-            ((1).[ν] ={⊤,⊤ ∖ ↑lftN}▷=∗ &{α} shift_loc l 1 ↦∗: ty_own ty tid).
+            ((1).[ν] ={⊤,⊤ ∖ ↑lftN}▷=∗ &{α} shift_loc l 1 ↦∗: ty_own ty tid) ∗
+            ∃ q'', ⌜(q' + q'' = 1)%Qp⌝ ∗ q''.[ν].
   Proof.
     iIntros "INV Hâ—¯".
     iDestruct "INV" as (st) "(H↦lrc & H● & INV)".
-    iAssert (∃ q' n, st ≡ Some (Cinr (to_agree ν, q', n)) ∗ ⌜q ≤ q'⌝%Qc)%I with
+    iAssert (∃ q' n, st ≡ Some (to_agree ν, Cinr (q', n)) ∗ ⌜q ≤ q'⌝%Qc)%I with
        "[#]" as (q' n) "[Hst %]".
     { iDestruct (own_valid_2 with "H● H◯") as %[[[=]|
-         (? & st' & [=<-] & -> & [Heq|Hle])]%option_included Hv]%auth_valid_discrete_2.
-      - iExists q, xH.  iSplit; iPureIntro. by constructor. done.
+       (? & [agν st'] & [=<-] & -> & [Heq|Hle])]%option_included Hv]%auth_valid_discrete_2.
+      - iExists q, xH. iSplit; iPureIntro. by constructor. done.
       - iClear "∗#".
-        revert Hle Hv=>/csum_included [ -> // | [[?[?[//]]] | [?[st''[Heq[-> Hle]]]]]].
-        revert Heq. intros [= <-]. destruct st'' as [[ag q'] n].
-        revert Hle=>/Some_included_2 /Some_pair_included
-           [/Some_pair_included_total_1 [/agree_included Heq Hqq'] _] [[Hag _] _].
+        revert Hle Hv=>/prod_included [/= /agree_included Hag /csum_included
+              [-> [//] | [[?[?[//]]] | [?[[q' n] [Heq [-> Hle]]]]]]] [Hagok _].
+        revert Heq. intros [= <-]. revert Hle=>/prod_included [/= Hqq' _].
         iExists q', n. iSplit.
-        + iPureIntro. do 4 constructor; last done.
-          apply agree_op_inv. by rewrite comm -Heq.
-        + revert Hqq'. by intros [<-%leibniz_equiv|?%frac_included_weak]%Some_included. }
+        + iPureIntro. rewrite (agree_op_inv agν) //. by rewrite comm -Hag.
+        + by revert Hqq'=>/frac_included_weak. }
     iDestruct "Hst" as %[st' [-> Hst']]%equiv_Some_inv_r'.
-    destruct st' as [|[[]]|]; try by inversion Hst'. apply (inj Cinr), (inj2 pair) in Hst'.
-    destruct Hst' as [[Hst' <-%leibniz_equiv]%(inj2 pair) <-%leibniz_equiv].
-    simpl. setoid_rewrite <-Hst'. clear Hst'.
-    iDestruct "INV" as (q'' ν') "(Hag & Hq'q'' & Hν & INV)".
+    destruct st' as [?[|[]|]]; destruct Hst' as [Hag Hst']; try by inversion Hst'.
+    apply (inj Cinr), (inj2 pair) in Hst'.
+    destruct Hst' as [<-%leibniz_equiv <-%leibniz_equiv]. simpl in *.
+    setoid_rewrite <-Hag. iDestruct "INV" as (ν') "(Hag & Hν & Hshr & Hq')".
     iDestruct "Hag" as %<-%(inj to_agree)%leibniz_equiv.
-    iDestruct "Hq'q''" as %Hq'q''. iExists _, _, _. rewrite own_op. iFrame. auto.
+    iExists q', n. rewrite own_op. by iFrame.
   Qed.
 
   (* Cloning a ref. We need to increment the counter. *)
@@ -77,12 +75,12 @@ Section ref_functions.
     rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
     iMod "H↦" as "[H↦1 H↦2]". wp_read. wp_let.
     iDestruct (refcell_inv_reading_inv with "INV Hâ—¯")
-      as (q' q'' n) "(H↦lrc & [H● H◯] & Hq'q'' & [Hν1 Hν2] & INV)".
-    wp_read. wp_let. wp_op. wp_write. iDestruct "Hq'q''" as %[Hq'q'' _].
-    iMod (own_update with "H●") as "[H● ?]".
+      as (q' n) "(H↦lrc & _ & [H● H◯] & Hshr' & H† & Hq')".
+    wp_read. wp_let. wp_op. wp_write. iDestruct "Hq'" as (q'') "(Hq'q'' & Hν1 & Hν2)".
+    iDestruct "Hq'q''" as %Hq'q''. iMod (own_update with "H●") as "[H● ?]".
     { apply auth_update_alloc,
-         (op_local_update_discrete _ _ (reading_st (q''/2)%Qp ν))=>-[[Hagv _]_].
-      split; [split|done].
+         (op_local_update_discrete _ _ (reading_st (q''/2)%Qp ν))=>-[Hagv _].
+      split; [|split; last done].
       - by rewrite /= agree_idemp.
       - change ((q''/2+q')%Qp ≤ 1%Qp)%Qc. rewrite -Hq'q'' comm -{2}(Qp_div_2 q'').
         apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q''/2)%Qp).
@@ -93,9 +91,11 @@ Section ref_functions.
     wp_let. wp_bind (_ <-{_} !_)%E. iApply (wp_memcpy with "[$Hlr $H↦]"); [done..|].
     iIntros "!>[Hlr H↦]". wp_seq.
     iMod ("Hcloseα2" with "[$H◯] Hna") as "[Hα2 Hna]".
-    iMod ("Hcloseδ" with "[H↦lrc H● Hν1 INV] Hna") as "[Hδ Hna]".
-    { iExists _. rewrite Z.add_comm. iFrame. iExists _, _. iFrame. simpl.
-      rewrite agree_idemp (comm Qp_plus) (assoc Qp_plus) Qp_div_2 (comm Qp_plus). auto. }
+    iMod ("Hcloseδ" with "[H↦lrc H● Hν1 Hshr' H†] Hna") as "[Hδ Hna]".
+    { iExists _. rewrite Z.add_comm. iFrame. iExists _. iFrame. iSplitR.
+      - rewrite /= agree_idemp. auto.
+      - iExists _. iFrame.
+        rewrite (comm Qp_plus) (assoc Qp_plus) Qp_div_2 (comm Qp_plus). auto. }
     iMod ("Hcloseβ" with "Hδ") as "Hβ". iMod ("Hcloseα1" with "[$H↦]") as "Hα1".
     iAssert (elctx_interp [☀ α; ☀ β] qE) with "[Hα1 Hα2 Hβ]" as "HE".
     { rewrite /elctx_interp big_sepL_cons big_sepL_singleton. iFrame. }
@@ -173,29 +173,28 @@ Section ref_functions.
     iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]". done.
     iMod (na_bor_acc with "LFT Hinv Hβ Hna") as "(INV & Hna & Hcloseβ)"; [done..|].
     iDestruct (refcell_inv_reading_inv with "INV [$Hâ—¯]")
-      as (q' q'' n) "(H↦lrc & H●◯ & >% & Hν' & Hshr & Hend)".
+      as (q' n) "(H↦lrc & >% & H●◯ & Hshr & H† & Hq')". iDestruct "Hq'" as (q'') ">[% Hν']".
     wp_read. wp_let. wp_op. wp_write.
     iAssert (|={⊤,⊤ ∖ ↑lftN}▷=> refcell_inv tid lrc γ β ty')%I
-      with "[H↦lrc H●◯ Hν Hν' Hshr Hend]" as "INV".
-    { iDestruct (own_valid with "H●◯")
-        as %[[Heq%(inj Cinr)|Hincl%csum_included]%Some_included Hv]%auth_valid_discrete_2.
-      - destruct Heq as [[_ ?%leibniz_equiv]?%leibniz_equiv]. simpl in *. subst.
+      with "[H↦lrc H●◯ Hν Hν' Hshr H†]" as "INV".
+    { iDestruct (own_valid with "H●◯") as %[[ _ [Heq%(inj Cinr)|Hincl%csum_included]
+        %Some_included]%Some_pair_included [_ Hv]]%auth_valid_discrete_2.
+      - destruct Heq as [?%leibniz_equiv ?%leibniz_equiv]. simpl in *. subst.
         iExists None. iFrame. iMod (own_update with "H●◯") as "$".
         { apply auth_update_dealloc. rewrite -(right_id None op (Some _)).
           apply op_local_update_cancellable_empty, _. }
-        iApply "Hend". replace 1%Qp with (q'+q'')%Qp by naive_solver. iFrame.
-      - destruct Hincl as [[=]|[(?&?&[=]&?)|(?&?&[=<-]&[=<-]&[[[ag q0]n']EQ])]].
-        rewrite EQ. destruct EQ as [[EQag ?%leibniz_equiv]?%leibniz_equiv].
-           simpl in *. subst.
+        iApply "H†". replace 1%Qp with (q'+q'')%Qp by naive_solver. iFrame.
+      - destruct Hincl as [ [=] |[ (?&?&[=]&?) | (?&?&[=<-]&[=<-]&[[q0 n']EQ]) ]].
+        destruct EQ as [?%leibniz_equiv ?%leibniz_equiv]. simpl in *. subst.
         iAssert (lrc ↦ #(Z.pos n'))%I with "[H↦lrc]" as "H↦lrc".
         { destruct n'; [|done..]. by rewrite /= Pos.pred_double_succ. }
-        iExists (Some (Cinr (ag, q0, n'))). iFrame. iMod (own_update with "H●◯") as "$".
-        { apply auth_update_dealloc. rewrite -Cinr_op Some_op.
+        iExists (Some (_, Cinr (q0, n'))). iFrame. iMod (own_update with "H●◯") as "$".
+        { apply auth_update_dealloc.
+          rewrite -(agree_idemp (to_agree _)) -pair_op -Cinr_op -pair_op Some_op.
           apply (op_local_update_cancellable_empty (reading_st q ν)), _. }
-        iExists (q+q'')%Qp, ν. iFrame. iApply step_fupd_intro; first done. iIntros "!>".
-        iSplit; iPureIntro.
-        + apply agree_op_inv. by rewrite comm -EQag.
-        + rewrite assoc (comm _ q0 q). by intuition. }
+        iExists ν. iFrame. iApply step_fupd_intro; first done. iIntros "!>".
+        iSplitR; first done. iExists (q+q'')%Qp. iFrame.
+        by rewrite assoc (comm _ q0 q). }
     wp_bind Endlft. iApply (wp_fupd_step with "INV"); [done..|]. wp_seq.
     iIntros "INV !>". wp_seq. iMod ("Hcloseβ" with "[$INV] Hna") as "[Hβ Hna]".
     iMod ("Hcloseα" with "Hβ") as "Hα".
diff --git a/theories/typing/unsafe/refcell/refcell.v b/theories/typing/unsafe/refcell/refcell.v
index e2df4a414f26f1760d635d8d29095a2926443ebb..8b8b4d65eaed6258ed874a349bc23efdb84a8021 100644
--- a/theories/typing/unsafe/refcell/refcell.v
+++ b/theories/typing/unsafe/refcell/refcell.v
@@ -6,20 +6,21 @@ From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Definition refcell_stR :=
-  optionUR (csumR (exclR unitC) (prodR (prodR (agreeR lftC) fracR) positiveR)).
+  optionUR (prodR (agreeR lftC) (csumR (exclR unitC) (prodR fracR positiveR))).
 Class refcellG Σ :=
   RefCellG :> inG Σ (authR refcell_stR).
 
 Definition Z_of_refcell_st (st : refcell_stR) : Z :=
   match st with
   | None => 0
-  | Some (Cinr (_, _, n)) => Zpos n
+  | Some (_, Cinr (_, n)) => Zpos n
   | Some _ => -1
   end.
 
 Definition reading_st (q : frac) (ν : lft) : refcell_stR :=
-  Some (Cinr (to_agree ν, q, xH)).
-Definition writing_st : refcell_stR := Some (Cinl (Excl ())).
+  Some (to_agree ν, Cinr (q, xH)).
+Definition writing_st (ν : lft) : refcell_stR :=
+  Some (to_agree ν, Cinl (Excl ())).
 
 Definition refcellN := lrustN .@ "refcell".
 Definition refcell_invN := refcellN .@ "inv".
@@ -30,12 +31,19 @@ Section refcell_inv.
   Definition refcell_inv tid (l : loc) (γ : gname) (α : lft) ty : iProp Σ :=
     (∃ st, l ↦ #(Z_of_refcell_st st) ∗ own γ (● st) ∗
       match st return _ with
-      | None => &{α}(shift_loc l 1 ↦∗: ty.(ty_own) tid)
-      | Some (Cinr (agν, q, n)) =>
-        ∃ q' ν, agν ≡ to_agree ν ∗ ⌜(q + q')%Qp = 1%Qp⌝ ∗ q'.[ν] ∗
-                ty.(ty_shr) (α ∪ ν) tid (shift_loc l 1) ∗
-                (1.[ν] ={⊤, ⊤∖↑lftN}▷=∗ &{α}(shift_loc l 1 ↦∗: ty.(ty_own) tid))
-      | Some _ => True
+      | None =>
+        (* Not borrowed. *)
+        &{α}(shift_loc l 1 ↦∗: ty.(ty_own) tid)
+      | Some (agν, st) =>
+        ∃ ν, agν ≡ to_agree ν ∗
+             (1.[ν] ={⊤, ⊤∖↑lftN}▷=∗ &{α}(shift_loc l 1 ↦∗: ty.(ty_own) tid)) ∗
+             match st with
+             | Cinr (q, n) =>
+               (* Immutably borrowed. *)
+               ty.(ty_shr) (α ∪ ν) tid (shift_loc l 1) ∗
+               ∃ q', ⌜(q + q')%Qp = 1%Qp⌝ ∗ q'.[ν]
+             | _ => (* Mutably borrowed. *) True
+             end
       end)%I.
 
   Global Instance refcell_inv_ne n tid l γ α :
@@ -60,11 +68,12 @@ Section refcell_inv.
       iSplit; iIntros "!>!#H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl;
       iFrame; by iApply "Hown". }
     iDestruct "H" as (st) "H"; iExists st;
-      iDestruct "H" as "($&$&H)"; destruct st as [[|[[]]|]|]; try done;
+      iDestruct "H" as "($&$&H)"; destruct st as [[agν st]|]; try done;
       last by iApply "Hb".
-    iDestruct "H" as (q' ν) "(Hag & Heq & Htok & Hs & Hh)". iExists q', ν.
-    iDestruct ("Hshr" with "Hs") as "$". iFrame. iIntros "H†".
-    iMod ("Hh" with "H†") as "Hh". iModIntro. iNext. iMod "Hh". by iApply "Hb".
+    iDestruct "H" as (ν) "(Hag & Hh & H)". iExists ν. iFrame. iSplitL "Hh".
+    { iIntros "Hν". iMod ("Hh" with "Hν") as "Hh". iModIntro. iNext.
+      iMod "Hh". by iApply "Hb". }
+    destruct st as [|[]|]; try done. iDestruct "H" as "[H $]". by iApply "Hshr".
   Qed.
 End refcell_inv.
 
@@ -102,26 +111,27 @@ Section refcell.
       as "[$ HQ]"; last first.
     { iMod ("Hclose" with "HQ []") as "[Hb $]".
       - iIntros "!> H !>". iNext. iDestruct "H" as (γ st) "(? & _ & _)".
-        iExists _. iIntros "{$H}!%". destruct st as [[|[[]?]|]|]; simpl; lia.
+        iExists _. iIntros "{$H}!%". destruct st as [[?[|[]|]]|]; simpl; lia.
       - iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
         iExists κ, γ. iSplitR. by iApply lft_incl_refl. by iApply bor_na. }
     clear dependent n. iDestruct "H" as ([|n|[]]) "[Hn >%]"; try lia.
     - iFrame. iMod (own_alloc (● None)) as (γ) "Hst". done. iExists γ, None. by iFrame.
     - iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". done.
-      iMod (own_alloc (● Some (Cinr (to_agree ν, (1/2)%Qp, n)))) as (γ) "Hst".
+      iMod (own_alloc (● Some (to_agree ν, Cinr ((1/2)%Qp, n)))) as (γ) "Hst".
       { by apply auth_auth_valid. }
       iMod (rebor _ _ (κ ∪ ν) with "LFT [] Hvl") as "[Hvl Hh]". done.
       { iApply lft_le_incl. apply gmultiset_union_subseteq_l. }
       iDestruct (lft_glb_acc with "Htok' Htok1") as (q') "[Htok Hclose]".
       iMod (ty_share with "LFT Hvl Htok") as "[Hshr Htok]". done.
       iDestruct ("Hclose" with "Htok") as "[$ Htok]".
-      iExists γ, _. iFrame "Hst Hn". iExists _, _. iIntros "{$Htok2 $Hshr}!>!>".
-      rewrite Qp_div_2. iSplit; first done. iSplit; first done. iIntros "Hν".
-      iMod ("Hhν" with "Hν") as "Hν". iModIntro. iNext. iMod "Hν".
+      iExists γ, _. iFrame "Hst Hn". iExists _. iIntros "{$Hshr}".
+      iSplitR; first by auto. iSplitR "Htok2"; last first.
+      { iExists _. iFrame. rewrite Qp_div_2. auto. }
+      iIntros "!> !> Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro. iNext. iMod "Hν".
       iApply fupd_mask_mono; last iApply "Hh". done. rewrite -lft_dead_or. auto.
-    - iMod (own_alloc (● Some (Cinl (Excl ())))) as (γ) "Hst".
-      { by apply auth_auth_valid. }
-      iFrame. iExists _, _. by iFrame.
+    - iMod (own_alloc (● writing_st static)) as (γ) "Hst". { by apply auth_auth_valid. }
+      iFrame. iExists _, _. iFrame. iExists _. iSplitR; first by auto.
+      iIntros "!>!> _". iApply step_fupd_intro; auto.
   Qed.
   Next Obligation.
     iIntros (?????) "LFT #Hκ H". iDestruct "H" as (α γ) "[#??]".
diff --git a/theories/typing/unsafe/refcell/refcell_code.v b/theories/typing/unsafe/refcell/refcell_code.v
index faf8ef0dd32fec39deb085ef186b7798a805daf3..396076aa1f2fdd951792dde4fda5694df4e885c3 100644
--- a/theories/typing/unsafe/refcell/refcell_code.v
+++ b/theories/typing/unsafe/refcell/refcell_code.v
@@ -176,21 +176,22 @@ Section refcell_functions.
                        ty_shr ty (β ∪ ν) tid (shift_loc lx 1) ∗
                        own γ (◯ reading_st qν ν) ∗ refcell_inv tid lx γ β ty)%I
         with ">[Hlx Hownst Hst Hβtok2]" as (q' ν) "(Hβtok2 & Hν & Hshr & Hreading & INV)".
-      { destruct st as [[|[[agν q] n]|]|]; try done.
-        - iDestruct "Hst" as (q' ν) "(Hag & #Hqq' & [Hν1 Hν2] & #Hshr & H†)".
+      { destruct st as [[agν [|[q n]|]]|]; try done.
+        - iDestruct "Hst" as (ν) "(Hag & H† & #Hshr & Hst)".
+          iDestruct "Hst" as (q') "(#Hqq' & [Hν1 Hν2])".
           iExists _, _. iFrame "Hν1". iDestruct "Hag" as %Hag. iDestruct "Hqq'" as %Hqq'.
           iMod (own_update with "Hownst") as "[Hownst ?]".
           { apply auth_update_alloc,
-               (op_local_update_discrete _ _ (reading_st (q'/2)%Qp ν))=>-[[Hagv _]_].
-            split; [split|].
+            (op_local_update_discrete _ _ (reading_st (q'/2)%Qp ν))=>-[Hagv _].
+            split; [|split].
             - by rewrite -Hag /= agree_idemp.
             - change ((q'/2+q)%Qp ≤ 1%Qp)%Qc. rewrite -Hqq' comm -{2}(Qp_div_2 q').
               apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q'/2)%Qp).
               apply Qcplus_le_mono_r, Qp_ge_0.
             - done. }
-          iFrame "∗#". iExists _. rewrite Z.add_comm /=. iFrame. iExists _, _. iFrame.
-          rewrite /= Hag agree_idemp (comm Qp_plus) (assoc Qp_plus) Qp_div_2
-                  (comm Qp_plus). auto.
+          iFrame "∗#". iExists _. rewrite Z.add_comm /=. iFrame. iExists _. iFrame.
+          iSplitR; first by rewrite /= Hag agree_idemp. iFrame "Hshr". iExists _. iFrame.
+          rewrite (comm Qp_plus) (assoc Qp_plus) Qp_div_2 (comm Qp_plus). auto.
         - iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". done.
           iMod (own_update with "Hownst") as "[Hownst Hreading]"; first by apply
             auth_update_alloc, (op_local_update_discrete _ _ (reading_st (1/2)%Qp ν)).
@@ -200,9 +201,10 @@ Section refcell_functions.
           { iApply lft_le_incl. apply gmultiset_union_subseteq_l. }
           iMod (ty_share with "LFT Hst Htok") as "[#Hshr Htok]". done. iFrame "Hshr".
           iDestruct ("Hclose" with "Htok") as "[$ Htok2]". iExists _. iFrame.
-          iExists _, _. iFrame. rewrite Qp_div_2. iSplitR; first done. iSplitR; first done.
-          iIntros "{$Hshr} !> Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro.
-          iNext. iMod "Hν". iApply "Hh". rewrite -lft_dead_or. auto. }
+          iExists _. iSplitR; first done. iFrame "Hshr". iSplitR "Htok2".
+          + iIntros "!> Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro.
+            iNext. iMod "Hν". iApply "Hh". rewrite -lft_dead_or. auto.
+          + iExists _. iFrame. by rewrite Qp_div_2. }
       iMod ("Hclose'" with "[$INV] Hna") as "[Hβtok1 Hna]".
       iAssert (elctx_interp [☀α] qE)%I with ">[Hclose Hβtok1 Hβtok2]" as "HE".
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
@@ -259,17 +261,22 @@ Section refcell_functions.
     rewrite {1}/elctx_interp big_sepL_singleton.
     iMod (lft_incl_acc with "Hαβ HE") as (qβ) "[Hβtok Hclose]". done.
     iMod (na_bor_acc with "LFT Hinv Hβtok Hna") as "(INV & Hna & Hclose')"; try done.
-    iDestruct "INV" as (st) "(Hlx & Hownst & Hst)". wp_read. wp_let. wp_op=>?; wp_if.
+    iDestruct "INV" as (st) "(Hlx & Hownst & Hb)". wp_read. wp_let. wp_op=>?; wp_if.
     - wp_write. wp_bind (new _). iApply wp_new; [done..|]. iNext.
       iIntros (lref vl) "(EQ & H† & Hlref)". iDestruct "EQ" as %?%(inj Z.of_nat 2%nat).
       destruct vl as [|?[|?[]]]; try done. wp_let.
       rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
       iDestruct "Hlref" as "[Hlref0 Hlref1]". wp_op. wp_write. wp_op. wp_write.
-      destruct st as [[|[[]]|]|]; try done.
+      destruct st as [[?[|[]|]]|]; try done.
+      iMod (lft_create with "LFT") as (ν) "[Htok #Hhν]". done.
       iMod (own_update with "Hownst") as "[Hownst ?]".
-      { apply auth_update_alloc, (op_local_update_discrete _ _ writing_st)=>//. }
-      iMod ("Hclose'" with "[Hlx Hownst] Hna") as "[Hβtok Hna]";
-        first by iExists _; iFrame.
+      { by eapply auth_update_alloc, (op_local_update_discrete _ _ (writing_st ν)). }
+      iMod (rebor _ _ (β ∪ ν) with "LFT [] Hb") as "[Hb Hbh]". done.
+      { iApply lft_le_incl. apply gmultiset_union_subseteq_l. }
+      iMod ("Hclose'" with "[Hlx Hownst Hbh] Hna") as "[Hβtok Hna]".
+      { iExists _. iFrame. iExists ν. iSplit; first by auto. iNext. iSplitL; last by auto.
+        iIntros "Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro. iNext. iMod "Hν".
+        iApply "Hbh". rewrite -lft_dead_or. auto. }
       iAssert (elctx_interp [☀α] qE)%I with ">[Hclose Hβtok]" as "HE".
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
       iApply (type_sum_memcpy [refmut α ty; unit] _ _ _ _ _ _ _ _
@@ -280,9 +287,10 @@ Section refcell_functions.
       { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame.
         rewrite tctx_hasty_val' //. rewrite /= freeable_sz_full. iFrame.
         iExists [_; _]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
-        iFrame. iExists _, _, _. iFrame "∗#". }
+        iFrame. iExists _, _, _, _. iFrame "#∗". iApply (bor_shorten with "[] [$Hb]").
+        iApply lft_glb_mono; first done. iApply lft_incl_refl. }
       simpl. eapply type_delete; [solve_typing..|]. eapply (type_jump [_]); solve_typing.
-    - iMod ("Hclose'" with "[Hlx Hownst Hst] Hna") as "[Hβtok Hna]";
+    - iMod ("Hclose'" with "[Hlx Hownst Hb] Hna") as "[Hβtok Hna]";
         first by iExists st; iFrame.
       iAssert (elctx_interp [☀α] qE)%I with ">[Hclose Hβtok]" as "HE".
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
diff --git a/theories/typing/unsafe/refcell/refmut.v b/theories/typing/unsafe/refcell/refmut.v
index 4076f85019fc904ba526bec8da02589fa0ab3627..db6c45d0aca621235a59cd3dd7135da0bcc22701 100644
--- a/theories/typing/unsafe/refcell/refmut.v
+++ b/theories/typing/unsafe/refcell/refmut.v
@@ -15,9 +15,9 @@ Section refmut.
        ty_own tid vl :=
          match vl return _ with
          | [ #(LitLoc lv);  #(LitLoc lrc) ] =>
-           ∃ γ β ty', &{β}(lv ↦∗: ty.(ty_own) tid) ∗
+           ∃ ν γ β ty', &{α ∪ ν}(lv ↦∗: ty.(ty_own) tid) ∗
              α ⊑ β ∗ &na{β, tid, refcell_invN}(refcell_inv tid lrc γ β ty') ∗
-             own γ (◯ writing_st)
+             1.[ν] ∗ own γ (◯ writing_st ν)
          | _ => False
          end;
        ty_shr κ tid l :=
@@ -35,10 +35,16 @@ Section refmut.
     iMod (bor_fracture (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦". done.
     destruct vl as [|[[|lv|]|][|[[|lrc|]|][]]];
       try by iMod (bor_persistent_tok with "LFT Hb Htok") as "[>[] _]".
+    iMod (bor_exists with "LFT Hb") as (ν) "Hb". done.
     iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
     iMod (bor_exists with "LFT Hb") as (β) "Hb". done.
     iMod (bor_exists with "LFT Hb") as (ty') "Hb". done.
-    rewrite (assoc _ _ (α ⊑ β)%I). iMod (bor_sep with "LFT Hb") as "[Hb _]". done.
+    rewrite (assoc _ _ (α ⊑ β)%I). iMod (bor_sep with "LFT Hb") as "[Hb H]". done.
+    rewrite (comm _ (1).[ν])%I. rewrite (assoc _ _ _ (1).[ν])%I.
+    iMod (bor_sep with "LFT H") as "[_ H]". done.
+    iMod (bor_fracture (λ q, (1 * q).[ν])%I with "LFT [H]") as "H". done.
+    { by rewrite Qp_mult_1_l. }
+    iDestruct (frac_bor_lft_incl _ _ 1 with "LFT H") as "#Hκν". iClear "H".
     iMod (bor_sep with "LFT Hb") as "[Hb Hαβ]". done.
     iMod (bor_persistent_tok with "LFT Hαβ Htok") as "[#Hαβ $]". done.
     iExists _, _. iFrame "H↦". rewrite {1}bor_unfold_idx.
@@ -52,7 +58,9 @@ Section refmut.
       { iApply bor_unfold_idx. eauto. }
       iModIntro. iNext. iMod "Hb".
       iMod (ty.(ty_share) with "LFT [Hb] Htok") as "[#Hshr $]". solve_ndisj.
-      { iApply bor_shorten; last done. iApply lft_glb_mono. done. iApply lft_incl_refl. }
+      { iApply bor_shorten; last done. rewrite -assoc.
+        iApply lft_glb_mono; first by iApply lft_incl_refl.
+        iApply lft_incl_glb; first done. iApply lft_incl_refl. }
       iMod ("Hclose" with "[]") as "_"; auto.
     - iMod ("Hclose" with "[]") as "_". by eauto.
       iApply step_fupd_intro. set_solver. auto.
@@ -88,10 +96,11 @@ Section refmut.
     iSplit; [|iSplit; iAlways].
     - done.
     - iIntros (tid [|[[]|][|[[]|][]]]); try iIntros "[]". iIntros "H".
-      iDestruct "H" as (γ β ty') "(Hb & #H⊑ & #Hinv & Hown)".
-      iExists γ, β, ty'. iFrame "∗#". iSplit.
-      + iApply bor_iff; last done.
-        iSplit; iIntros "!>!# H"; iDestruct "H" as (vl) "[??]";
+      iDestruct "H" as (ν γ β ty') "(Hb & #H⊑ & #Hinv & Hν & Hown)".
+      iExists ν, γ, β, ty'. iFrame "∗#". iSplit.
+      + iApply bor_shorten; last iApply bor_iff; last done.
+        * iApply lft_glb_mono; first done. iApply lft_incl_refl.
+        * iSplit; iIntros "!>!# H"; iDestruct "H" as (vl) "[??]";
           iExists vl; iFrame; by iApply "Ho".
       + by iApply lft_incl_trans.
     - iIntros (κ tid l) "H". iDestruct "H" as (lv lrc) "H". iExists lv, lrc.
diff --git a/theories/typing/unsafe/refcell/refmut_code.v b/theories/typing/unsafe/refcell/refmut_code.v
new file mode 100644
index 0000000000000000000000000000000000000000..8d29b53cd55a46ed6b5628dfaf585eeec5b05880
--- /dev/null
+++ b/theories/typing/unsafe/refcell/refmut_code.v
@@ -0,0 +1,161 @@
+From Coq.QArith Require Import Qcanon.
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import auth csum frac agree.
+From iris.base_logic Require Import big_op fractional.
+From lrust.lifetime Require Import na_borrow.
+From lrust.typing Require Import typing.
+From lrust.typing.unsafe.refcell Require Import refcell refmut.
+Set Default Proof Using "Type".
+
+Section refmut_functions.
+  Context `{typeG Σ, refcellG Σ}.
+
+  (* TODO : map, when we will have a nice story about closures. *)
+
+  (* Turning a refmut into a shared borrow. *)
+  Definition refmut_deref : val :=
+    funrec: <> ["x"] :=
+      let: "x'" := !"x" in
+      let: "r'" := !"x'" in
+      letalloc: "r" <- "r'" in
+      delete [ #1; "x"];; "return" ["r"].
+
+  Lemma refmut_deref_type ty :
+    typed_instruction_ty [] [] [] refmut_deref
+      (fn (fun '(α, β) => [☀α; ☀β; α ⊑ β])%EL
+          (fun '(α, β) => [# &shr{α}(refmut β ty)]%T)
+          (fun '(α, β) => &shr{α}ty)%T).
+  Proof.
+    apply type_fn; [apply _..|]. move=>/= [α β] ret arg. inv_vec arg=>x. simpl_subst.
+    eapply type_deref; [solve_typing..|by apply read_own_move|done|]=>x'.
+    iIntros "!# * #LFT Hna HE HL Hk HT". simpl_subst.
+    rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
+    iDestruct "HT" as "[Hx Hx']".
+    destruct x' as [[|lx'|]|]; try iDestruct "Hx'" as "[]".
+    iDestruct "Hx'" as (lv lrc) "#(Hfrac & #Hshr)".
+    rewrite {1}/elctx_interp 2!big_sepL_cons big_sepL_singleton.
+    iDestruct "HE" as "([Hα1 Hα2] & Hβ & #Hαβ)".
+    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_glb_acc with "Hβ Hα2") as (qβα) "[Hα2β Hcloseβα2]".
+    wp_bind (!(LitV lx'))%E. iApply (wp_fupd_step 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]".
+    iMod ("Hcloseα1" with "[$H↦1 $H↦2]") as "Hα1".
+    iAssert (elctx_interp [☀ α; ☀ β; α ⊑ β] qE) with "[Hα1 Hα2 Hβ Hαβ]" as "HE".
+    { rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
+    iApply (type_letalloc_1 (&shr{α}ty) _
+        [ x ◁ box (uninit 1); #lv ◁ &shr{α}ty]%TC with "LFT Hna HE HL Hk");
+      [solve_typing..| |]; first last.
+    { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
+      iFrame. iApply (ty_shr_mono with "LFT [] Hshr'"). iApply lft_incl_glb; first done.
+      iApply lft_incl_refl. }
+    intros r. simpl_subst. eapply type_delete; [solve_typing..|].
+    eapply (type_jump [_]); solve_typing.
+  Qed.
+
+  (* Turning a refmut into a unique borrow. *)
+  Definition refmut_derefmut : val :=
+    funrec: <> ["x"] :=
+      let: "x'" := !"x" in
+      let: "r'" := !"x'" in
+      letalloc: "r" <- "r'" in
+      delete [ #1; "x"];; "return" ["r"].
+
+  Lemma refmut_derefmut_type ty :
+    typed_instruction_ty [] [] [] refmut_deref
+      (fn (fun '(α, β) => [☀α; ☀β; α ⊑ β])%EL
+          (fun '(α, β) => [# &uniq{α}(refmut β ty)]%T)
+          (fun '(α, β) => &uniq{α}ty)%T).
+  Proof.
+    apply type_fn; [apply _..|]. move=>/= [α β] ret arg. inv_vec arg=>x. simpl_subst.
+    eapply type_deref; [solve_typing..|by apply read_own_move|done|]=>x'.
+    iIntros "!# * #LFT Hna HE HL Hk HT". simpl_subst.
+    rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
+    iDestruct "HT" as "[Hx Hx']".
+    rewrite {1}/elctx_interp 2!big_sepL_cons big_sepL_singleton.
+    iDestruct "HE" as "(Hα & Hβ & #Hαβ)".
+    destruct x' as [[|lx'|]|]; try iDestruct "Hx'" as "[]".
+    iMod (bor_exists with "LFT Hx'") as (vl) "H". done.
+    iMod (bor_sep with "LFT H") as "[H↦ H]". done.
+    destruct vl as [|[[|lv|]|][|[[|lrc|]|][]]];
+      try by iMod (bor_persistent_tok with "LFT H Hα") as "[>[] _]".
+    iMod (bor_exists with "LFT H") as (ν) "H". done.
+    iMod (bor_exists with "LFT H") as (γ) "H". done.
+    iMod (bor_exists with "LFT H") as (δ) "H". done.
+    iMod (bor_exists with "LFT H") as (ty') "H". done.
+    iMod (bor_sep with "LFT H") as "[Hb H]". done.
+    iMod (bor_sep with "LFT H") as "[Hβδ H]". done.
+    iMod (bor_persistent_tok with "LFT Hβδ Hα") as "[#Hβδ Hα]". done.
+    rewrite (comm _ (1).[ν])%I. rewrite (assoc _ _ _ (1).[ν])%I.
+    iMod (bor_sep with "LFT H") as "[_ H]". done.
+    iMod (bor_fracture (λ q, (1 * q).[ν])%I with "LFT [H]") as "H". done.
+    { by rewrite Qp_mult_1_l. }
+    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]");
+      [done| |by iApply (bor_unnest with "LFT Hb")|]; first done.
+    wp_read. iIntros "Hb !>". wp_let.
+    iMod ("Hcloseα" with "[$H↦]") as "[_ Hα]".
+    iAssert (elctx_interp [☀ α; ☀ β; α ⊑ β] qE) with "[Hα Hβ Hαβ]" as "HE".
+    { rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
+    iApply (type_letalloc_1 (&uniq{α}ty) _
+        [ x ◁ box (uninit 1); #lv ◁ &uniq{α}ty]%TC with "LFT Hna HE HL Hk");
+      [solve_typing..| |]; first last.
+    { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
+      iFrame. iApply (bor_shorten with "[] Hb").
+      by iApply lft_incl_glb; [iApply lft_incl_glb|iApply lft_incl_refl]. }
+    intros r. simpl_subst. eapply type_delete; [solve_typing..|].
+    eapply (type_jump [_]); solve_typing.
+  Qed.
+
+  (* Dropping a refmut and set the count to 0 in the corresponding refcell. *)
+  Definition refmut_drop : val :=
+    funrec: <> ["x"] :=
+      let: "rc" := !("x" +â‚— #1) in
+      "rc" <- #0;;
+      Endlft;;
+      delete [ #2; "x"];;
+      let: "r" := new [ #0] in "return" ["r"].
+
+  Lemma refmut_drop_type ty :
+    typed_instruction_ty [] [] [] refmut_drop
+      (fn (fun α => [☀α])%EL (fun α => [# refmut α ty])  (fun α => unit)).
+  Proof.
+    apply type_fn; [apply _..|]. move=>/= α ret arg. inv_vec arg=>x. simpl_subst.
+    iIntros "!# * #LFT Hna Hα HL Hk Hx".
+    rewrite {1}/elctx_interp big_sepL_singleton tctx_interp_singleton tctx_hasty_val.
+    destruct x as [[|lx|]|]; try iDestruct "Hx" as "[]". iDestruct "Hx" as "[Hx Hx†]".
+    iDestruct "Hx" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Hx"; try iDestruct "Hx" as "[_ >[]]".
+    rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+    iDestruct "Hx" as "[[Hx↦1 Hx↦2] Hx]". wp_op. wp_read. wp_let.
+    iDestruct "Hx" as (ν γ β ty') "(Hb & #Hαβ & #Hinv & Hν & H◯)".
+    iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]". done.
+    iMod (na_bor_acc with "LFT Hinv Hβ Hna") as "(INV & Hna & Hcloseβ)"; [done..|].
+    iDestruct "INV" as (st) "(H↦lrc & H● & INV)". wp_write.
+    iDestruct (own_valid_2 with "H● H◯") as %[[[=]| (? & [agν st'] & [=<-] & -> &
+      [[Hag Heq]|[_ Hle]%prod_included])]%option_included []]%auth_valid_discrete_2;
+      last first.
+    { by destruct (exclusive_included (Cinl (Excl ())) st'). }
+    setoid_subst. iDestruct "INV" as (ν') "(Hνν' & H† & _)".
+    iDestruct "Hνν'" as %<-%(inj to_agree)%leibniz_equiv.
+    wp_bind Endlft. iApply (wp_fupd_step with "[H† Hν]");
+      [done| |iApply ("H†" with "Hν")|]; first done.
+    wp_seq. iIntros "{Hb} Hb !>".
+    iMod ("Hcloseβ" with ">[H↦lrc H● H◯ Hb] Hna") as "[Hβ Hna]".
+    { iExists None. iFrame. iMod (own_update_2 with "H● H◯") as "$"; last done.
+      apply auth_update_dealloc. rewrite -(right_id None _ (Some _)).
+      apply op_local_update_cancellable_empty, _. }
+    iMod ("Hcloseα" with "Hβ") as "Hα". wp_seq.
+    iAssert (elctx_interp [☀ α] qE) with "[Hα]" as "HE".
+    { by rewrite /elctx_interp big_sepL_singleton. }
+    iApply (type_delete _ _ [ #lx ◁ box (uninit 2)]%TC with "LFT Hna HE HL Hk");
+      [solve_typing..| |]; first last.
+    { rewrite tctx_interp_singleton tctx_hasty_val' //. iFrame. iExists [ #lv;#lrc].
+      rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton uninit_own. iFrame. auto. }
+    eapply type_new; [solve_typing..|]=>r. simpl_subst.
+    eapply (type_jump [_]); solve_typing.
+  Qed.
+End refmut_functions.