diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 85e83cfb8df5372a2fcaafcdb533c7ab6f05d143..8680f75dab080dddd3e4e7da492957397ee4aaef 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -47,10 +47,7 @@ Section uniq_bor.
   Next Obligation.
     intros κ0 ty κ κ' tid l. iIntros "#LFT #Hκ #H".
     iDestruct "H" as (l') "[Hfb Hvs]". iAssert (κ0∪κ' ⊑ κ0∪κ)%I as "#Hκ0".
-    { iApply (lft_incl_glb with "[] []").
-      - iApply lft_le_incl. apply gmultiset_union_subseteq_l.
-      - iApply (lft_incl_trans with "[] Hκ").
-        iApply lft_le_incl. apply gmultiset_union_subseteq_r. }
+    { iApply lft_glb_mono. iApply lft_incl_refl. done. }
     iExists l'. iSplit. by iApply (frac_bor_shorten with "[]").
     iIntros "!# * % Htok".
     iApply (step_fupd_mask_mono F _ _ (F∖↑shrN∖↑lftN)); try set_solver.
diff --git a/theories/typing/unsafe/refcell.v b/theories/typing/unsafe/refcell.v
index b2a8a7170f674fabeb74ae625c9e07dce74936fd..d670fe966e42fd1b2375a7e5463645bd370e268e 100644
--- a/theories/typing/unsafe/refcell.v
+++ b/theories/typing/unsafe/refcell.v
@@ -21,7 +21,7 @@ Definition Z_of_refcell_st (st : refcell_stR) : Z :=
 
 Definition reading_st (q : frac) (κ : lft) : refcell_stR :=
   Some (Cinr (to_agree (κ : leibnizC lft), q, xH)).
-Definition writing_st (q : frac) : refcell_stR := Some (Cinl (Excl ())).
+Definition writing_st : refcell_stR := Some (Cinl (Excl ())).
 
 Definition refcellN := nroot .@ "refcell".
 Definition refcell_invN := refcellN .@ "inv".
@@ -187,11 +187,11 @@ Section ref.
          | _ => False
          end;
        ty_shr κ tid l :=
-         ▷ ∃ ν q γ β ty' (lv lrc : loc),
-           κ ⊑ ν ∗ &frac{κ} (λ q, l↦∗{q} [ #lv; #lrc]) ∗
-           ty.(ty_shr) (α ∪ ν) tid lv ∗
-           α ⊑ β ∗ &na{β, tid, refcell_invN}(refcell_inv tid lrc γ β ty') ∗
-           &na{κ, tid, refcell_refN}(own γ (◯ reading_st q ν)) |}%I.
+          ∃ ν q γ β ty' (lv lrc : loc),
+             κ ⊑ ν ∗ &frac{κ} (λ q, l↦∗{q} [ #lv; #lrc]) ∗
+             ▷ ty.(ty_shr) (α ∪ ν) tid lv ∗
+             ▷ (α ⊑ β) ∗ ▷ &na{β, tid, refcell_invN}(refcell_inv tid lrc γ β ty') ∗
+             &na{κ, tid, refcell_refN}(own γ (◯ reading_st q ν)) |}%I.
   Next Obligation.
     iIntros (???[|[[]|][|[[]|][]]]); try iIntros "[]". by iIntros "_".
   Qed.
@@ -223,7 +223,7 @@ Section ref.
   Next Obligation.
     iIntros (??????) "#? #? H". iDestruct "H" as (ν q γ β ty' lv lrc) "H".
     iExists _, _, _, _, _, _, _. iDestruct "H" as "#(? & ? & $ & $ & $ & ?)".
-    iNext. iSplit; last iSplit.
+    iSplit; last iSplit.
     - by iApply lft_incl_trans.
     - by iApply frac_bor_shorten.
     - by iApply na_bor_shorten.
@@ -233,17 +233,16 @@ Section ref.
   Proof.
     intros n ?? EQ. unfold ref. split; [split|]=>//=.
     - f_contractive=>tid vl. repeat (f_contractive || f_equiv). apply EQ.
-    - intros κ tid l. f_contractive. repeat f_equiv. apply EQ.
+    - intros κ tid l. repeat (f_contractive || f_equiv). apply EQ.
   Qed.
   Global Instance ref_ne n α : Proper (dist n ==> dist n) (ref α).
   Proof. apply contractive_ne, _. Qed.
 
   Global Instance ref_mono E L :
-    Proper (flip (lctx_lft_incl E L) ==> eqtype E L ==> subtype E L) ref.
+    Proper (flip (lctx_lft_incl E L) ==> subtype E L ==> subtype E L) ref.
   Proof.
     iIntros (α1 α2 Hα ty1 ty2 Hty) "#LFT #HE #HL".
-    pose proof Hty as Hty'%eqtype_unfold.
-    iDestruct (Hty' with "LFT HE HL") as "(%&#Ho&#Hs)".
+    iDestruct (Hty with "LFT HE HL") as "(%&#Ho&#Hs)".
     iDestruct (Hα with "HE HL") as "Hα1α2".
     iSplit; [|iSplit; iAlways].
     - done.
@@ -253,26 +252,142 @@ Section ref.
       + iApply ty_shr_mono; last by iApply "Hs". done.
         iApply lft_glb_mono. done. iApply lft_incl_refl.
       + by iApply lft_incl_trans.
-    - iIntros (κ tid l) "H". iNext. iDestruct "H" as (ν q γ β ty' lv lrc) "H".
+    - iIntros (κ tid l) "H". iDestruct "H" as (ν q γ β ty' lv lrc) "H".
       iExists ν, q, γ, β, ty', lv, lrc. iDestruct "H" as "#($&$&?&?&$&$)". iSplit.
       + iApply ty_shr_mono; last by iApply "Hs". done.
         iApply lft_glb_mono. done. iApply lft_incl_refl.
       + by iApply lft_incl_trans.
   Qed.
   Global Instance ref_mono_flip E L :
-    Proper (lctx_lft_incl E L ==> flip (eqtype E L) ==> flip (subtype E L)) ref.
+    Proper (lctx_lft_incl E L ==> flip (subtype E L) ==> flip (subtype E L)) ref.
   Proof. intros ??????. by apply ref_mono. Qed.
   Lemma ref_mono' E L α1 α2 ty1 ty2 :
-    lctx_lft_incl E L α2 α1 → eqtype E L ty1 ty2 →
+    lctx_lft_incl E L α2 α1 → subtype E L ty1 ty2 →
     subtype E L (ref α1 ty1) (ref α2 ty2).
   Proof. intros. by eapply ref_mono. Qed.
   Global Instance ref_proper E L :
     Proper (lctx_lft_eq E L ==> eqtype E L ==> eqtype E L) ref.
-  Proof. intros ??[]???. split; by apply ref_mono'. Qed.
+  Proof. intros ??[]?? EQ. split; apply ref_mono'; try done; apply EQ. Qed.
   Lemma ref_proper' E L α1 α2 ty1 ty2 :
     lctx_lft_eq E L α1 α2 → eqtype E L ty1 ty2 →
     eqtype E L (ref α1 ty1) (ref α2 ty2).
   Proof. intros. by eapply ref_proper. Qed.
 End ref.
 
-Hint Resolve refcell_mono' refcell_proper' ref_mono' ref_proper' : lrust_typing.
+Definition refcell_refmutN := refcellN .@ "refmut".
+
+Section refmut.
+  Context `{typeG Σ, refcellG Σ}.
+  Local Hint Extern 1000 (_ ⊆ _) => set_solver : ndisj.
+
+  Program Definition refmut (α : lft) (ty : type) :=
+    {| ty_size := 2;
+       ty_own tid vl :=
+         match vl return _ with
+         | [ #(LitLoc lv);  #(LitLoc lrc) ] =>
+           ∃ γ β ty', &{β}(lv ↦∗: ty.(ty_own) tid) ∗
+             α ⊑ β ∗ &na{β, tid, refcell_invN}(refcell_inv tid lrc γ β ty') ∗
+             own γ (◯ writing_st)
+         | _ => False
+         end;
+       ty_shr κ tid l :=
+         ∃ (lv lrc : loc),
+           &frac{κ} (λ q, l↦∗{q} [ #lv; #lrc]) ∗
+           □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[α ∪ κ]
+             ={F, F∖↑shrN∖↑lftN}▷=∗ ty.(ty_shr) (α ∪ κ) tid lv ∗ q.[α ∪ κ] |}%I.
+  Next Obligation.
+    iIntros (???[|[[]|][|[[]|][]]]); try iIntros "[]". by iIntros "_".
+  Qed.
+  Next Obligation.
+    iIntros (α ty E κ l tid q HE) "#LFT Hb Htok".
+    iMod (bor_exists with "LFT Hb") as (vl) "Hb". done.
+    iMod (bor_sep with "LFT Hb") as "[H↦ Hb]". done.
+    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 (ty') "Hb". done.
+    rewrite (assoc _ _ (α ⊑ β)%I). iMod (bor_sep with "LFT Hb") as "[Hb _]". done.
+    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.
+    iDestruct "Hb" as (i) "[#Hpb Hpbown]".
+    iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ ty_shr ty (α ∪ κ) tid lv)%I
+          with "[Hpbown]") as "#Hinv"; first by eauto.
+    iIntros "!> !# * % Htok". clear HE.
+    iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
+    iDestruct "INV" as "[>Hbtok|#Hshr]".
+    - iMod (bor_unnest with "LFT [Hbtok]") as "Hb". solve_ndisj.
+      { 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. }
+      iMod ("Hclose" with "[]") as "_"; auto.
+    - iMod ("Hclose" with "[]") as "_". by eauto.
+      iApply step_fupd_intro. set_solver. auto.
+  Qed.
+  Next Obligation.
+    iIntros (??????) "#? #? H". iDestruct "H" as (lv lrc) "[#Hf #H]".
+    iExists _, _. iSplit.
+    - by iApply frac_bor_shorten.
+    - iIntros "!# * % Htok".
+      iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]". set_solver.
+      { iApply lft_glb_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_glb_mono. iApply lft_incl_refl. done.
+  Qed.
+
+  Global Instance refmut_contractive α : Contractive (refmut α).
+  Proof.
+    intros n ?? EQ. unfold refmut. split; [split|]=>//=.
+    - f_contractive=>tid vl. repeat (f_contractive || f_equiv). apply EQ.
+    - intros κ tid l. repeat (f_contractive || f_equiv). apply EQ.
+  Qed.
+  Global Instance refmut_ne n α : Proper (dist n ==> dist n) (refmut α).
+  Proof. apply contractive_ne, _. Qed.
+
+  Global Instance refmut_mono E L :
+    Proper (flip (lctx_lft_incl E L) ==> eqtype E L ==> subtype E L) refmut.
+  Proof.
+    iIntros (α1 α2 Hα ty1 ty2 Hty) "#LFT #HE #HL".
+    pose proof Hty as Hty'%eqtype_unfold.
+    iDestruct (Hty' with "LFT HE HL") as "(%&#Ho&#Hs)".
+    iDestruct (Hα with "HE HL") as "Hα1α2".
+    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_proper; last done.
+        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.
+      iDestruct "H" as "[$ #H]". iIntros "!# * % Htok".
+      iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]". set_solver.
+      { iApply lft_glb_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_glb_mono. done. iApply lft_incl_refl.
+      by iApply "Hs".
+  Qed.
+  Global Instance refmut_mono_flip E L :
+    Proper (lctx_lft_incl E L ==> eqtype E L ==> flip (subtype E L)) refmut.
+  Proof. intros ??????. by apply refmut_mono. Qed.
+  Lemma refmut_mono' E L α1 α2 ty1 ty2 :
+    lctx_lft_incl E L α2 α1 → eqtype E L ty1 ty2 →
+    subtype E L (refmut α1 ty1) (refmut α2 ty2) .
+  Proof. intros. by eapply refmut_mono. Qed.
+  Global Instance refmut_proper E L :
+    Proper (lctx_lft_eq E L ==> eqtype E L ==> eqtype E  L) refmut.
+  Proof. intros ??[]???. split; by apply refmut_mono'. Qed.
+  Lemma refmut_proper' E L α1 α2 ty1 ty2 :
+    lctx_lft_eq E L α1 α2 → eqtype E L ty1 ty2 →
+    eqtype E L (ref α1 ty1) (ref α2 ty2).
+  Proof. intros. by eapply ref_proper. Qed.
+End refmut.
+
+Hint Resolve refcell_mono' refcell_proper' ref_mono' ref_proper'
+             refmut_mono' refmut_proper' : lrust_typing.