diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index c4e26967f4f4b997466a2d512e4d8a6d228666f9..0efccc1614f7ad134586e8fbb2f2c71f48bb9829 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -23,7 +23,7 @@ Implicit Types κ : lft.
 Lemma bor_acc_cons E q κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ} P -∗ q.[κ] ={E}=∗ ▷ P ∗
-    ∀ Q, ▷ Q -∗ ▷(▷ Q ={⊤∖↑lftN}=∗ ▷ P) ={E}=∗ &{κ} Q ∗ q.[κ].
+    ∀ Q, ▷ Q -∗ ▷(▷ Q ={∅}=∗ ▷ P) ={E}=∗ &{κ} Q ∗ q.[κ].
 Proof.
   iIntros (?) "#LFT HP Htok".
   iMod (bor_acc_strong with "LFT HP Htok") as (κ') "(#Hκκ' & $ & Hclose)"; first done.
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 4684b65d115f0ae967368e629234dcd33e5d3632..54cddeac8f82078d5dff603ff8b5f2152afff2cf 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -86,7 +86,7 @@ Module Type lifetime_sig.
   Parameter lft_dead_static : [† static] -∗ False.
 
   Parameter lft_create : ∀ E, ↑lftN ⊆ E →
-    lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={⊤,⊤∖↑lftN}▷=∗ [†κ]).
+    lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={↑lftN,∅}▷=∗ [†κ]).
   Parameter bor_create : ∀ E κ P,
     ↑lftN ⊆ E → lft_ctx -∗ ▷ P ={E}=∗ &{κ} P ∗ ([†κ] ={E}=∗ ▷ P).
   Parameter bor_fake : ∀ E κ P,
@@ -119,11 +119,11 @@ Module Type lifetime_sig.
                 ([†κ] ∗ |={E∖↑lftN,E}=> idx_bor_own q i).
   Parameter bor_acc_strong : ∀ E q κ P, ↑lftN ⊆ E →
     lft_ctx -∗ &{κ} P -∗ q.[κ] ={E}=∗ ∃ κ', κ ⊑ κ' ∗ ▷ P ∗
-      ∀ Q, ▷ Q -∗ ▷(▷ Q -∗ [†κ'] ={⊤∖↑lftN}=∗ ▷ P) ={E}=∗ &{κ'} Q ∗ q.[κ].
+      ∀ Q, ▷ Q -∗ ▷(▷ Q -∗ [†κ'] ={∅}=∗ ▷ P) ={E}=∗ &{κ'} Q ∗ q.[κ].
   Parameter bor_acc_atomic_strong : ∀ E κ P, ↑lftN ⊆ E →
     lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
       (∃ κ', κ ⊑ κ' ∗ ▷ P ∗
-         ∀ Q, ▷ Q -∗ ▷ (▷ Q -∗ [†κ'] ={⊤∖↑lftN}=∗ ▷ P) ={E∖↑lftN,E}=∗ &{κ'} Q) ∨
+         ∀ Q, ▷ Q -∗ ▷ (▷ Q -∗ [†κ'] ={∅}=∗ ▷ P) ={E∖↑lftN,E}=∗ &{κ'} Q) ∨
            ([†κ] ∗ |={E∖↑lftN,E}=> True).
 
   (* Because Coq's module system is horrible, we have to repeat properties of lft_incl here
@@ -148,7 +148,7 @@ Module Type lifetime_sig.
     ↑lftN ⊆ E → lft_ctx -∗ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}Φ x.
   Parameter bor_acc_atomic_cons : ∀ E κ P,
     ↑lftN ⊆ E → lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
-      (▷ P ∗ ∀ Q, ▷ Q -∗ ▷ (▷ Q ={⊤∖↑lftN}=∗ ▷ P) ={E∖↑lftN,E}=∗ &{κ} Q) ∨
+      (▷ P ∗ ∀ Q, ▷ Q -∗ ▷ (▷ Q ={∅}=∗ ▷ P) ={E∖↑lftN,E}=∗ &{κ} Q) ∨
       ([†κ] ∗ |={E∖↑lftN,E}=> True).
   Parameter bor_acc_atomic : ∀ E κ P,
     ↑lftN ⊆ E → lft_ctx -∗ &{κ}P ={E,E∖↑lftN}=∗
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index b3b74823938427a48cd96861012214619dc76eb7..95012c54969fe8ee7486fc23755347be1a9a1bde 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -56,13 +56,13 @@ Proof.
 Qed.
 
 Lemma add_vs Pb Pb' P Q Pi κ :
-  ▷ ▷ (Pb ≡ (P ∗ Pb')) -∗ ▷ lft_vs κ Pb Pi -∗ ▷ (▷ Q -∗ [†κ] ={⊤∖↑lftN}=∗ ▷ P) -∗
+  ▷ ▷ (Pb ≡ (P ∗ Pb')) -∗ ▷ lft_vs κ Pb Pi -∗ ▷ (▷ Q -∗ [†κ] ={∅}=∗ ▷ P) -∗
   ▷ lft_vs κ (Q ∗ Pb') Pi.
 Proof.
   iIntros "#HEQ Hvs HvsQ". iNext. rewrite !lft_vs_unfold.
   iDestruct "Hvs" as (n) "[Hcnt Hvs]". iExists n.
   iIntros "{$Hcnt}*Hinv[HQ HPb] #H†". iApply fupd_trans.
-  iApply fupd_mask_mono; last iMod ("HvsQ" with "HQ H†") as "HP". solve_ndisj.
+  iApply fupd_mask_mono; last iMod ("HvsQ" with "HQ H†") as "HP". set_solver.
   iModIntro. iAssert (â–· Pb)%I with "[HPb HP]" as "HPb".
   { iNext. iRewrite "HEQ". iFrame. }
   iApply ("Hvs" with "Hinv HPb H†").
@@ -152,7 +152,7 @@ Qed.
 Lemma bor_acc_strong E q κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ} P -∗ q.[κ] ={E}=∗ ∃ κ', κ ⊑ κ' ∗ ▷ P ∗
-    ∀ Q, ▷ Q -∗ ▷(▷ Q -∗ [†κ'] ={⊤∖↑lftN}=∗ ▷ P) ={E}=∗ &{κ'} Q ∗ q.[κ].
+    ∀ Q, ▷ Q -∗ ▷(▷ Q -∗ [†κ'] ={∅}=∗ ▷ P) ={E}=∗ &{κ'} Q ∗ q.[κ].
 Proof.
   unfold bor, raw_bor. iIntros (HE) "#LFT Hbor Htok".
   iDestruct "Hbor" as (κ'') "(#Hle & Htmp)". iDestruct "Htmp" as (s'') "(Hbor & #Hs)".
@@ -219,7 +219,7 @@ Lemma bor_acc_atomic_strong E κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
    (∃ κ', κ ⊑ κ' ∗ ▷ P ∗
-      ∀ Q, ▷ Q -∗ ▷ (▷ Q -∗ [†κ'] ={⊤∖↑lftN}=∗ ▷ P) ={E∖↑lftN,E}=∗ &{κ'} Q) ∨
+      ∀ Q, ▷ Q -∗ ▷ (▷ Q -∗ [†κ'] ={∅}=∗ ▷ P) ={E∖↑lftN,E}=∗ &{κ'} Q) ∨
     ([†κ] ∗ |={E∖↑lftN,E}=> True).
 Proof.
   iIntros (HE) "#LFT Hbor". rewrite bor_unfold_idx /idx_bor /bor /raw_bor.
@@ -270,7 +270,7 @@ Qed.
 Lemma bor_acc_atomic_cons E κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
-    (▷ P ∗ ∀ Q, ▷ Q -∗ ▷ (▷ Q ={⊤∖↑lftN}=∗ ▷ P) ={E∖↑lftN,E}=∗ &{κ} Q) ∨
+    (▷ P ∗ ∀ Q, ▷ Q -∗ ▷ (▷ Q ={∅}=∗ ▷ P) ={E∖↑lftN,E}=∗ &{κ} Q) ∨
     ([†κ] ∗ |={E∖↑lftN,E}=> True).
 Proof.
   iIntros (?) "#LFT HP".
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index e731f97ab0cbfbc106d5c67f765bd5a958e7265c..f4a620bcf1041a21ac4ee38c3bb20de01bdfac8c 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -17,7 +17,7 @@ Lemma lft_kill (I : gmap lft lft_names) (K K' : gset lft) (κ : lft) :
     ([∗ set] κ' ∈ K', lft_inv_dead κ'))%I in
   (∀ κ', is_Some (I !! κ') → κ' ⊂ κ → κ' ∈ K) →
   (∀ κ', is_Some (I !! κ') → κ ⊂ κ' → κ' ∈ K') →
-  Iinv -∗ lft_inv_alive κ -∗ [†κ] ={⊤∖↑mgmtN}=∗ Iinv ∗ lft_inv_dead κ.
+  Iinv -∗ lft_inv_alive κ -∗ [†κ] ={↑borN ∪ ↑inhN}=∗ Iinv ∗ lft_inv_dead κ.
 Proof.
   iIntros (Iinv HK HK') "(HI & Halive & Hdead) Hlalive Hκ".
   rewrite lft_inv_alive_unfold;
@@ -34,12 +34,13 @@ Proof.
     rewrite /lft_inv_dead; iDestruct "Hdead" as (R) "(_ & Hcnt' & _)".
     iDestruct (own_cnt_valid_2 with "Hcnt' Hcnt")
       as %[?%nat_included _]%auth_valid_discrete_2; omega. }
-  iMod (box_empty with "Hbox") as "[HP Hbox]"=>//; first solve_ndisj.
+  iMod (box_empty with "Hbox") as "[HP Hbox]"=>//; first set_solver.
   { intros i s. by rewrite lookup_fmap fmap_Some=> -[? [/HB -> ->]]. }
   rewrite lft_vs_unfold; iDestruct "Hvs" as (n) "[Hcnt Hvs]".
   iDestruct (big_sepS_filter_acc (⊂ κ) _ _ (dom _ I) with "Halive")
     as "[Halive Halive']".
   { intros κ'. rewrite elem_of_dom. eauto. }
+  iApply fupd_trans. iApply fupd_mask_mono; first by apply union_subseteq_l.
   iMod ("Hvs" $! I with "[HI Halive Hbox Hbor] HP Hκ") as "(Hinv & HQ & Hcnt')".
   { rewrite lft_vs_inv_unfold. iFrame. rewrite /lft_bor_dead.
     iExists (dom _ B), P. rewrite !to_gmap_dom -map_fmap_compose.
@@ -50,7 +51,7 @@ Proof.
   iMod (own_cnt_update_2 with "Hcnt Hcnt'") as "?".
   { apply auth_update_dealloc, (nat_local_update _ _ 0 0); omega. }
   rewrite /Iinv. iFrame "Hdead Halive' HI".
-  iMod (lft_inh_kill with "[$Hinh $HQ]"); first solve_ndisj.
+  iModIntro. iMod (lft_inh_kill with "[$Hinh $HQ]"); first set_solver+.
   iModIntro. rewrite /lft_inv_dead. iExists Q. by iFrame.
 Qed.
 
@@ -60,7 +61,7 @@ Lemma lfts_kill A (I : gmap lft lft_names) (K K' : gset lft) :
   (∀ κ κ', κ ∈ K → lft_alive_in A κ → is_Some (I !! κ') →
     κ' ∉ K → κ' ⊂ κ → κ' ∈ K') →
   Iinv K' -∗ ([∗ set] κ ∈ K, lft_inv A κ ∗ [†κ])
-    ={⊤∖↑mgmtN}=∗ Iinv K' ∗ [∗ set] κ ∈ K, lft_inv_dead κ.
+    ={↑borN ∪ ↑inhN}=∗ Iinv K' ∗ [∗ set] κ ∈ K, lft_inv_dead κ.
 Proof.
   intros Iinv. revert K'.
   induction (collection_wf K) as [K _ IH]=> K' HK HK'.
@@ -132,7 +133,7 @@ Proof. intros κ [??]%elem_of_down_close. by apply elem_of_dom. Qed.
 
 Lemma lft_create E :
   ↑lftN ⊆ E →
-  lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={⊤,⊤∖↑lftN}▷=∗ [†κ]).
+  lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={↑lftN,∅}▷=∗ [†κ]).
 Proof.
   iIntros (?) "#LFT".
   iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
@@ -150,7 +151,7 @@ Proof.
   iModIntro; iExists {[ Λ ]}.
   rewrite {1}/lft_tok big_sepMS_singleton. iFrame "HΛ".
   clear I A HΛ. iIntros "!# HΛ".
-  iApply (step_fupd_mask_mono ⊤ _ _ (⊤∖↑mgmtN)); [solve_ndisj..|].
+  iApply (step_fupd_mask_mono (↑lftN) _ _ (↑lftN∖↑mgmtN));  [set_solver..|].
   iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
   rewrite /lft_tok big_sepMS_singleton.
   iDestruct (own_valid_2 with "HA HΛ")
@@ -169,14 +170,16 @@ Proof.
   { iApply (@big_sepS_impl with "[$HinvD]"); iIntros "!#".
     iIntros (κ Hκ) "?". iApply lft_inv_alive_in; last done.
     eauto using down_close_lft_alive_in. }
-  iAssert ([∗ set] κ ∈ K, lft_inv A κ ∗ [† κ])%I with "[HinvK]" as "HinvK". 
+  iAssert ([∗ set] κ ∈ K, lft_inv A κ ∗ [† κ])%I with "[HinvK]" as "HinvK".
   { iApply (@big_sepS_impl with "[$HinvK]"); iIntros "!#".
     iIntros (κ [? _]%elem_of_kill_set) "$". rewrite /lft_dead. eauto. }
+  iApply fupd_trans. iApply (fupd_mask_mono (↑borN ∪ ↑inhN));
+                       first by apply union_least; solve_ndisj.
   iMod (lfts_kill A I K K' with "[$HI $HinvD] HinvK") as "[[HI HinvD] HinvK]".
   { intros κ κ' [??]%elem_of_kill_set ??. apply elem_of_kill_set.
     split; last done. by eapply gmultiset_elem_of_subseteq. }
   { intros κ κ' ?????. apply elem_of_down_close; eauto 10. }
-  iMod ("Hclose" with "[-]") as "_"; last first.
+  iModIntro. iMod ("Hclose" with "[-]") as "_"; last first.
   { iModIntro. rewrite /lft_dead. iExists Λ.
     rewrite elem_of_singleton. auto. }
   iNext. iExists (<[Λ:=false]>A), I.
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index e4a59714b23349a25ad148a55d42fefa7eb24b3a..9c81827977c89c8191b22f8961516d4061be3fab 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -133,7 +133,7 @@ Section defs.
        own_cnt κ (● n) ∗
        ∀ I : gmap lft lft_names,
          lft_vs_inv_go κ lft_inv_alive I -∗ ▷ Pb -∗ lft_dead κ
-           ={⊤∖↑mgmtN}=∗
+           ={↑borN}=∗
          lft_vs_inv_go κ lft_inv_alive I ∗ ▷ Pi ∗ own_cnt κ (◯ n))%I.
 
   Definition lft_inv_alive_go (κ : lft)
@@ -263,7 +263,7 @@ Lemma lft_vs_unfold κ Pb Pi :
   lft_vs κ Pb Pi ⊣⊢ ∃ n : nat,
     own_cnt κ (● n) ∗
     ∀ I : gmap lft lft_names,
-      lft_vs_inv κ I -∗ ▷ Pb -∗ lft_dead κ ={⊤∖↑mgmtN}=∗
+      lft_vs_inv κ I -∗ ▷ Pb -∗ lft_dead κ ={↑borN}=∗
       lft_vs_inv κ I ∗ ▷ Pi ∗ own_cnt κ (◯ n).
 Proof. done. Qed.
 
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index e6df1d52529270ef3295cf28820cec75a997ae39..cc70c535dc8759fe1a6b15aa14a3e189d3d1102e 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -490,7 +490,7 @@ Qed.
 (* TODO RJ: Are there still places where this lemma
    is re-proven inline? *)
 Lemma lft_vs_cons q κ Pb Pb' Pi :
-  (lft_bor_dead κ ∗ ▷ Pb' ={⊤ ∖ ↑mgmtN}=∗ lft_bor_dead κ ∗ ▷ Pb) -∗
+  (lft_bor_dead κ ∗ ▷ Pb' ={↑borN}=∗ lft_bor_dead κ ∗ ▷ Pb) -∗
   ▷?q lft_vs κ Pb Pi -∗ ▷?q lft_vs κ Pb' Pi.
 Proof.
   iIntros "Hcons Hvs". iNext. rewrite !lft_vs_unfold.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index e7632f58b4f4713ef57beabb80e292d3dbe8eb57..ae8dbde0ee8fd9cacffa0302dde4633f3aa03d81 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -105,7 +105,7 @@ Section lft_contexts.
 
   Definition llctx_elt_interp (x : llctx_elt) (q : Qp) : iProp Σ :=
     let κ' := foldr (∪) static (x.2) in
-    (∃ κ0, ⌜x.1 = κ' ∪ κ0⌝ ∗ q.[κ0] ∗ □ (1.[κ0] ={⊤,⊤∖↑lftN}▷=∗ [†κ0]))%I.
+    (∃ κ0, ⌜x.1 = κ' ∪ κ0⌝ ∗ q.[κ0] ∗ □ (1.[κ0] ={↑lftN,∅}▷=∗ [†κ0]))%I.
   Global Instance llctx_elt_interp_fractional x :
     Fractional (llctx_elt_interp x).
   Proof.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index e610b8bf381b46b06f85a023a777630a8cc343a5..2c52aba10fe7f52b61071d0233f48ff44c6a1481 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -168,7 +168,8 @@ Section typing_rules.
     rewrite /llctx_interp big_sepL_cons. iIntros "[Hκ HL] HC HT".
     iDestruct "Hκ" as (Λ) "(% & Htok & #Hend)".
     iSpecialize ("Hend" with "Htok"). wp_bind Endlft.
-    iApply (wp_fupd_step with "Hend"); try done. wp_seq.
+    iApply (wp_mask_mono (↑lftN)); first done.
+    iApply (wp_fupd_step with "Hend"). done. set_solver. wp_seq.
     iIntros "#Hdead !>". wp_seq. iApply ("He" with "LFT Htl HE HL HC >").
     iApply (Hub with "[] HT"). simpl in *. subst κ. rewrite -lft_dead_or. auto.
   Qed.
diff --git a/theories/typing/unsafe/refcell/ref_code.v b/theories/typing/unsafe/refcell/ref_code.v
index 113af696c6e4472a23827540c4fe08279ca5b7f1..f740e8eb69c75462fed2fed39f55931e81a69af8 100644
--- a/theories/typing/unsafe/refcell/ref_code.v
+++ b/theories/typing/unsafe/refcell/ref_code.v
@@ -16,7 +16,7 @@ Section ref_functions.
     ∃ (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â—¯".
@@ -172,7 +172,7 @@ Section ref_functions.
     iDestruct (refcell_inv_reading_inv with "INV [$Hâ—¯]")
       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
+    iAssert (|={↑lftN,∅}▷=> refcell_inv tid lrc γ β ty')%I
       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.
@@ -189,10 +189,11 @@ Section ref_functions.
         { apply auth_update_dealloc.
           rewrite -(agree_idemp (to_agree _)) -pair_op -Cinr_op -pair_op Some_op.
           apply (cancel_local_update_empty (reading_st q ν)), _. }
-        iExists ν. iFrame. iApply step_fupd_intro; first done. iIntros "!>".
+        iExists ν. iFrame. iApply step_fupd_intro; first set_solver. 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.
+    wp_bind Endlft. iApply (wp_mask_mono (↑lftN)); first done.
+    iApply (wp_fupd_step with "INV"); [set_solver..|]. wp_seq.
     iIntros "INV !>". wp_seq. iMod ("Hcloseβ" with "[$INV] Hna") as "[Hβ Hna]".
     iMod ("Hcloseα" with "Hβ") as "Hα".
     iApply (type_type _ _ _ [ #lx ◁ box (uninit 2)]%TC with "[] LFT Hna [Hα] HL Hk");
diff --git a/theories/typing/unsafe/refcell/refcell.v b/theories/typing/unsafe/refcell/refcell.v
index 2101ab0ccd5fde03774ea4065e15403d0573431b..6ccdd17ea4f6ef58f4edde35ada9ce5d9d045f72 100644
--- a/theories/typing/unsafe/refcell/refcell.v
+++ b/theories/typing/unsafe/refcell/refcell.v
@@ -39,7 +39,7 @@ Section refcell_inv.
         &{α}(shift_loc l 1 ↦∗: ty.(ty_own) tid)
       | Some (agν, st) =>
         ∃ ν, agν ≡ to_agree ν ∗
-             (1.[ν] ={⊤, ⊤∖↑lftN}▷=∗ &{α}(shift_loc l 1 ↦∗: ty.(ty_own) tid)) ∗
+             (1.[ν] ={↑lftN,∅}▷=∗ &{α}(shift_loc l 1 ↦∗: ty.(ty_own) tid)) ∗
              match st with
              | Cinr (q, n) =>
                (* Immutably borrowed. *)
@@ -129,6 +129,7 @@ Section refcell.
     - iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". done.
       iMod (own_alloc (● Some (to_agree ν, Cinr ((1/2)%Qp, n)))) as (γ) "Hst".
       { by apply auth_auth_valid. }
+      iApply (fupd_mask_mono (↑lftN)); first done.
       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]".
@@ -141,7 +142,7 @@ Section refcell.
       iApply fupd_mask_mono; last iApply "Hh". done. rewrite -lft_dead_or. auto.
     - 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.
+      iIntros "!>!> _". iApply step_fupd_intro; [set_solver|auto].
   Qed.
   Next Obligation.
     iIntros (?????) "#Hκ H". iDestruct "H" as (α γ) "[#??]".
diff --git a/theories/typing/unsafe/refcell/refcell_code.v b/theories/typing/unsafe/refcell/refcell_code.v
index 5a12ad7f7a876cf68274f5030851e6ba20575ef4..8d1d4d4ef25c80fbc415703ba72db809a58e3600 100644
--- a/theories/typing/unsafe/refcell/refcell_code.v
+++ b/theories/typing/unsafe/refcell/refcell_code.v
@@ -204,6 +204,7 @@ Section refcell_functions.
             auth_update_alloc, (op_local_update_discrete _ _ (reading_st (1/2)%Qp ν)).
           rewrite right_id. iExists _, _. iFrame "Htok1 Hreading".
           iDestruct (lft_glb_acc with "Hβtok2 Htok2") as (q) "[Htok Hclose]".
+          iApply (fupd_mask_mono (↑lftN)); first done.
           iMod (rebor _ _ (β ∪ ν) with "LFT [] Hst") as "[Hst Hh]". done.
           { iApply lft_le_incl. apply gmultiset_union_subseteq_l. }
           iMod (ty_share with "LFT Hst Htok") as "[#Hshr Htok]". done. iFrame "Hshr".
@@ -280,9 +281,10 @@ Section refcell_functions.
       iMod (lft_create with "LFT") as (ν) "[Htok #Hhν]". done.
       iMod (own_update with "Hownst") as "[Hownst ?]".
       { by eapply auth_update_alloc, (op_local_update_discrete _ _ (writing_st ν)). }
+      iApply fupd_wp. iApply (fupd_mask_mono (↑lftN)); first done.
       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]".
+      iModIntro. 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. }
diff --git a/theories/typing/unsafe/refcell/refmut_code.v b/theories/typing/unsafe/refcell/refmut_code.v
index 14214350793008bc921a2843d939e24ec71dc7bc..e4102353a35f10914972f04c7f7a1a7af2aab94d 100644
--- a/theories/typing/unsafe/refcell/refmut_code.v
+++ b/theories/typing/unsafe/refcell/refmut_code.v
@@ -137,8 +137,9 @@ Section refmut_functions.
     { 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_bind Endlft. iApply (wp_mask_mono (↑lftN)); first done.
+    iApply (wp_fupd_step with "[H† Hν]");
+      [done| |iApply ("H†" with "Hν")|]; first set_solver.
     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.
diff --git a/theories/typing/unsafe/rwlock/rwlock.v b/theories/typing/unsafe/rwlock/rwlock.v
index dc70a67ca0f57a3f66cf6da29cf92638ddceaba2..3ce0d9f404a17aa341274155f722abe16e77740a 100644
--- a/theories/typing/unsafe/rwlock/rwlock.v
+++ b/theories/typing/unsafe/rwlock/rwlock.v
@@ -39,7 +39,7 @@ Section rwlock_inv.
       | Some (Cinr (agν, q, n)) =>
         (* Locked for read. *)
         ∃ (ν : lft) q', agν ≡ to_agree ν ∗
-                □ (1.[ν] ={⊤, ⊤∖↑lftN}▷=∗ [†ν]) ∗
+                □ (1.[ν] ={↑lftN,∅}▷=∗ [†ν]) ∗
                 ([†ν] ={↑lftN}=∗ &{α}(shift_loc l 1 ↦∗: ty.(ty_own) tid)) ∗
                 ty.(ty_shr) (α ∪ ν) tid (shift_loc l 1) ∗
                 ⌜(q + q')%Qp = 1%Qp⌝ ∗ q'.[ν]
diff --git a/theories/typing/unsafe/rwlock/rwlock_code.v b/theories/typing/unsafe/rwlock/rwlock_code.v
index 620554ebdd72be3974a194b3292dc94c6e5a5bd6..46aa4d6fc62a083c1fcc0fdfc453bcc0ef7e3aa9 100644
--- a/theories/typing/unsafe/rwlock/rwlock_code.v
+++ b/theories/typing/unsafe/rwlock/rwlock_code.v
@@ -188,7 +188,7 @@ Section rwlock_functions.
         iAssert (∃ qν ν, (qβ / 2).[β] ∗ (qν).[ν] ∗
                          ty_shr ty (β ∪ ν) tid (shift_loc lx 1) ∗
                          own γ (◯ reading_st qν ν) ∗ rwlock_inv tid lx γ β ty ∗
-                         ((1).[ν] ={⊤,⊤ ∖ ↑lftN}▷=∗ [†ν]))%I
+                         ((1).[ν] ={↑lftN,∅}▷=∗ [†ν]))%I
           with ">[Hlx Hownst Hst Hβtok2]"
           as (q' ν) "(Hβtok2 & Hν & Hshr & Hreading & INV & H†)".
         { destruct st' as [[|[[agν q] n]|]|]; try done.
diff --git a/theories/typing/unsafe/rwlock/rwlockreadguard.v b/theories/typing/unsafe/rwlock/rwlockreadguard.v
index d35d40f88c7b58259758a52a780e402d9d4cfb2a..21f9a717a50fb95fe7453e95e307197626071f03 100644
--- a/theories/typing/unsafe/rwlock/rwlockreadguard.v
+++ b/theories/typing/unsafe/rwlock/rwlockreadguard.v
@@ -23,7 +23,7 @@ Section rwlockreadguard.
            ∃ ν q γ β, ty.(ty_shr) (α ∪ ν) tid (shift_loc l 1) ∗
              α ⊑ β ∗ &shr{β,rwlockN}(rwlock_inv tid l γ β ty) ∗
              q.[ν] ∗ own γ (◯ reading_st q ν) ∗
-             (1.[ν] ={⊤, ⊤∖↑lftN}▷=∗ [†ν])
+             (1.[ν] ={↑lftN,∅}▷=∗ [†ν])
          | _ => False
          end;
        ty_shr κ tid l :=
diff --git a/theories/typing/unsafe/rwlock/rwlockreadguard_code.v b/theories/typing/unsafe/rwlock/rwlockreadguard_code.v
index becd1f1868b6bcbd8d87d407e153d1a8b63e1c37..f7c493bb2017641e5df59b573955db77b0b9489b 100644
--- a/theories/typing/unsafe/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/unsafe/rwlock/rwlockreadguard_code.v
@@ -97,15 +97,13 @@ Section rwlockreadguard_functions.
           iDestruct "Hst" as (ν' q') "(>EQν & _ & Hh & _ & >Hq & >Hν')".
           rewrite -EQ. iDestruct "EQν" as %<-%(inj to_agree)%leibniz_equiv.
           iCombine "Hν" "Hν'" as "Hν". iDestruct "Hq" as %->.
-          (* FIXME : here, I REALLY need to end a lifetime while an
-             invariant is still open. *)
-          iAssert (|={⊤,⊤ ∖ ↑lftN}▷=> lx' ↦ #0 ==∗ rwlock_inv tid lx' γ β ty)%I
-            with "[-]" as "?"; last admit.
+          iApply (step_fupd_mask_mono (↑lftN ∪ (⊤ ∖ ↑rwlockN ∖ ↑lftN)));
+            last iApply (step_fupd_mask_frame_r _ ∅); [try set_solver..|];
+            [apply union_least; solve_ndisj|].
           iMod ("H†" with "Hν") as "H†". iModIntro. iNext. iMod "H†".
-          iApply fupd_mask_mono; last iMod ("Hh" with "H†") as "Hb". done.
-          iIntros "!> Hlx". iExists None. iFrame. iApply (own_update_2 with "H● H◯").
-          apply auth_update_dealloc. rewrite -(right_id None op (Some _)).
-          apply cancel_local_update_empty, _.
+          iMod ("Hh" with "H†") as "Hb". iIntros "!> Hlx". iExists None. iFrame.
+          iApply (own_update_2 with "H● H◯"). apply auth_update_dealloc.
+          rewrite -(right_id None op (Some _)). apply cancel_local_update_empty, _.
         - iApply step_fupd_intro. set_solver. iNext. iIntros "Hlx".
           apply csum_included in Hle.
           destruct Hle as [|[(?&?&[=]&?)|(?&[[agν q']n]&[=<-]&->&Hle%prod_included)]];
@@ -144,5 +142,5 @@ Section rwlockreadguard_functions.
                 tctx_hasty_val' //. iFrame. iExists _, _, _, _. iFrame "∗#". }
       { rewrite /elctx_interp big_sepL_singleton //. }
       iApply (type_jump []); solve_typing.
-  Admitted.
+  Qed.
 End rwlockreadguard_functions.