diff --git a/opam b/opam
index 2c0379ff395b734cb461d4066f19a359c51710c6..bfd5401dcd263a55c69d1a4817f58560fa254f49 100644
--- a/opam
+++ b/opam
@@ -14,7 +14,7 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2020-06-19.0.80be7f21") | (= "dev") }
+  "coq-iris" { (= "dev.2020-07-02.0.59a1ad49") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index 26eee18171b9ed420e6cc6e76782b6e9c09a767c..183cdd37a6c5b2430a2e9086c3d8c6f52daacc4c 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -116,7 +116,7 @@ Qed.
 
 Lemma bor_later E κ P :
   ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ}(▷ P) ={E,E∖↑lftN}▷=∗ &{κ}P.
+  lft_ctx -∗ &{κ}(▷ P) ={E}[E∖↑lftN]▷=∗ &{κ}P.
 Proof.
   iIntros (?) "#LFT Hb".
   iMod (bor_acc_atomic_cons with "LFT Hb") as "[H|[H† Hclose]]"; first done.
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 5374ca71d7aba07a39c876f5a697f9d2b0de4fcb..b7b0abf7bb393148272b98515c0c195cf6a5b311 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -96,7 +96,7 @@ Module Type lifetime_sig.
   Parameter lft_dead_static : [† static] -∗ False.
 
   Parameter lft_create : ∀ E, ↑lftN ⊆ E →
-    lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={↑lftN,↑lft_userN}▷=∗ [†κ]).
+    lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={↑lftN}[↑lft_userN]▷=∗ [†κ]).
   Parameter bor_create : ∀ E κ P,
     ↑lftN ⊆ E → lft_ctx -∗ ▷ P ={E}=∗ &{κ} P ∗ ([†κ] ={E}=∗ ▷ P).
   Parameter bor_fake : ∀ E κ P,
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 383ed012c5a1c798a8ed649d01d45f7b6f74c9b6..92016023e6c12daf252f02f4cbd85aca69b2595f 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -110,7 +110,7 @@ Proof. by rewrite /kill_set elem_of_filter elem_of_dom. Qed.
 
 Lemma lft_create E :
   ↑lftN ⊆ E →
-  lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={↑lftN,↑lft_userN}▷=∗ [†κ]).
+  lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={↑lftN}[↑lft_userN]▷=∗ [†κ]).
 Proof.
   iIntros (?) "#LFT".
   iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
@@ -128,7 +128,7 @@ Proof.
   iModIntro; iExists {[ Λ ]}.
   rewrite {1}/lft_tok big_sepMS_singleton. iFrame "HΛ".
   clear I A HΛ. iIntros "!# HΛ".
-  iApply (step_fupd_mask_mono (↑lftN) _ _ (↑lftN∖↑mgmtN)); [solve_ndisj..|].
+  iApply (step_fupd_mask_mono (↑lftN) _ (↑lftN∖↑mgmtN)); [solve_ndisj..|].
   iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
   rewrite /lft_tok big_sepMS_singleton.
   iDestruct (own_valid_2 with "HA HΛ")
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 033c00f65dda1bce944860a1048c2530dfe600a9..3017ca810ad7c2bc01b5759354ecee60465f0af7 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -41,7 +41,7 @@ Section lft_contexts.
   (* Local lifetime contexts. *)
   Definition llctx_elt_interp (x : llctx_elt) (q : Qp) : iProp Σ :=
     let κ' := lft_intersect_list (x.2) in
-    (∃ κ0, ⌜x.1 = κ' ⊓ κ0⌝ ∗ q.[κ0] ∗ □ (1.[κ0] ={↑lftN,↑lft_userN}▷=∗ [†κ0]))%I.
+    (∃ κ0, ⌜x.1 = κ' ⊓ κ0⌝ ∗ q.[κ0] ∗ □ (1.[κ0] ={↑lftN}[↑lft_userN]▷=∗ [†κ0]))%I.
   Global Instance llctx_elt_interp_fractional x :
     Fractional (llctx_elt_interp x).
   Proof.
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 7a0f07c2b72f3ee8381ca7ea1c1d2be597982db1..09a3d7630025083cf8d37eef0a8970630a85bcee 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -27,7 +27,7 @@ Section arc.
      (*    because [weak_new] cannot prove ty_shr, even for a dead *)
      (*    lifetime. *)
      (ty.(ty_shr) ν tid (l +ₗ 2) ∨ [†ν]) ∗
-     □ (1.[ν] ={↑lftN ∪ ↑arc_endN,↑lft_userN}▷=∗
+     □ (1.[ν] ={↑lftN ∪ ↑arc_endN}[↑lft_userN]▷=∗
           [†ν] ∗ ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗ † l…(2 + ty.(ty_size))))%I.
 
   Global Instance arc_persist_ne tid ν γ l n :
@@ -103,7 +103,7 @@ Section arc.
        ty_shr κ tid l :=
          ∃ (l' : loc), &frac{κ} (λ q, l ↦{q} #l') ∗
            □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[κ]
-             ={F, F∖↑shrN}▷=∗ q.[κ] ∗ ∃ γ ν q', κ ⊑ ν ∗
+             ={F}[F∖↑shrN]▷=∗ q.[κ] ∗ ∃ γ ν q', κ ⊑ ν ∗
                 arc_persist tid ν γ l' ty ∗
                 &at{κ, arc_shrN}(arc_tok γ q')
     |}%I.
@@ -225,7 +225,7 @@ Section arc.
        ty_shr κ tid l :=
          ∃ (l' : loc), &frac{κ} (λ q, l ↦{q} #l') ∗
            □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[κ]
-             ={F, F∖↑shrN}▷=∗ q.[κ] ∗ ∃ γ ν,
+             ={F}[F∖↑shrN]▷=∗ q.[κ] ∗ ∃ γ ν,
                 arc_persist tid ν γ l' ty ∗ &at{κ, arc_shrN}(weak_tok γ)
     |}%I.
   Next Obligation. by iIntros (ty tid [|[[]|][]]) "H". Qed.
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index 1f30e5f0b941fc80f3ed6ea6aaa55423f098fb8b..d0f2e34e39f0c4892a7bbfaa7a6a26fc6f196e5e 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -40,7 +40,7 @@ Section mguard.
        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.[α⊓κ]
+                ={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. *)
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index ddf5a89333a2001c2023dae8027b457254f9a407..529b04c8703ac2f229f0799b748b200129caf780 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -85,7 +85,7 @@ Section rc.
                  because [weak_new] cannot prove ty_shr, even for a dead
                  lifetime. *)
               (ty.(ty_shr) ν tid (l +ₗ 2) ∨ [†ν]) ∗
-              □ (1.[ν] ={↑lftN,↑lft_userN}▷=∗ [†ν]))%I.
+              □ (1.[ν] ={↑lftN}[↑lft_userN]▷=∗ [†ν]))%I.
 
   Global Instance rc_persist_persistent : Persistent (rc_persist tid ν γ l ty).
   Proof. unfold rc_persist, tc_opaque. apply _. Qed.
@@ -123,7 +123,7 @@ Section rc.
        ty_shr κ tid l :=
          ∃ (l' : loc), &frac{κ} (λ q, l ↦{q} #l') ∗
            □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[κ]
-             ={F, F∖↑shrN}▷=∗ q.[κ] ∗ ∃ γ ν q', κ ⊑ ν ∗
+             ={F}[F∖↑shrN]▷=∗ q.[κ] ∗ ∃ γ ν q', κ ⊑ ν ∗
                 rc_persist tid ν γ l' ty ∗
                 &na{κ, tid, rc_shrN}(own γ (rc_tok q'))
     |}%I.
@@ -247,16 +247,16 @@ Section code.
         (((⌜strong = 1%positive⌝ ∗
            (∃ weak : Z, (l +ₗ 1) ↦ #weak ∗
              ((⌜weak = 1⌝ ∗
-               |={⊤,↑lft_userN}▷=> † l…(2 + ty.(ty_size)) ∗
+               |={⊤}[↑lft_userN]▷=> † l…(2 + ty.(ty_size)) ∗
                           ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗ na_own tid F) ∨
              (⌜weak > 1⌝ ∗
               ((l ↦ #1 -∗ (l +ₗ 1) ↦ #weak
                 ={⊤}=∗ na_own tid F ∗ ty_own (rc ty) tid [ #l ]) ∧
                (l ↦ #0 -∗ (l +ₗ 1) ↦ #(weak - 1)
-                ={⊤,↑lft_userN}▷=∗ ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗
+                ={⊤}[↑lft_userN]▷=∗ ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗
                 ((l +ₗ 2) ↦∗: (λ vl, ⌜length vl = ty.(ty_size)⌝)
                  ={⊤}=∗ na_own tid F)))))) ∧
-           (l ↦ #0 ={⊤,↑lft_userN}▷=∗
+           (l ↦ #0 ={⊤}[↑lft_userN]▷=∗
              ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗ † l…(2 + ty.(ty_size)) ∗ na_own tid F ∗
              (na_own tid F ={⊤}=∗ ∃ weak : Z,
                 (l +ₗ 1) ↦ #weak ∗
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index e79b788501aa09d8cd8e30930682bb8e52c2f892..e70716071d9330882256389019a630dd9c843d9b 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -20,7 +20,7 @@ Section weak.
        ty_shr κ tid l :=
          ∃ (l' : loc), &frac{κ} (λ q, l ↦{q} #l') ∗
            □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[κ]
-             ={F, F∖↑shrN}▷=∗ q.[κ] ∗ ∃ γ ν, rc_persist tid ν γ l' ty ∗
+             ={F}[F∖↑shrN]▷=∗ q.[κ] ∗ ∃ γ ν, rc_persist tid ν γ l' ty ∗
                 &na{κ, tid, rc_shrN}(own γ weak_tok)
     |}%I.
   Next Obligation. by iIntros (ty tid [|[[]|][]]) "H". Qed.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 7dc1047648a55ed467ee492c1c08080fe885309b..5ad3cb6592fcd4aae40537b7c5736762add25e7e 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -15,7 +15,7 @@ Section ref_functions.
     own γ (◯ reading_stR q ν) -∗
     ∃ (q' : Qp) n, l ↦ #(Zpos n) ∗ ⌜(q ≤ q')%Qc⌝ ∗
             own γ (● (refcell_st_to_R $ Some (ν, false, q', n)) ⋅ ◯ reading_stR q ν) ∗
-            ((1).[ν] ={↑lftN,↑lft_userN}▷=∗ &{α}((l +ₗ 1) ↦∗: ty_own ty tid)) ∗
+            ((1).[ν] ={↑lftN}[↑lft_userN]▷=∗ &{α}((l +ₗ 1) ↦∗: ty_own ty tid)) ∗
             (∃ q'', ⌜(q' + q'' = 1)%Qp⌝ ∗ q''.[ν]) ∗
             ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1).
   Proof.
@@ -162,7 +162,7 @@ Section ref_functions.
       as (q' n) "(H↦lrc & >% & H●◯ & H† & Hq' & Hshr)".
     iDestruct "Hq'" as (q'') ">[% Hν']".
     wp_read. wp_let. wp_op. wp_write.
-    iAssert (|={↑lftN,↑lft_userN}▷=> refcell_inv tid lrc γ β ty')%I
+    iAssert (|={↑lftN}[↑lft_userN]▷=> refcell_inv tid lrc γ β ty')%I
       with "[H↦lrc H●◯ Hν Hν' Hshr H†]" as "INV".
     { iDestruct (own_valid with "H●◯") as
           %[[[[_ ?]?]|[[_ [q0 Hq0]]%prod_included [n' Hn']]%prod_included]
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index c8acaf22704f3506566f21588e03e659f8ce8f15..27a92d38b6124c569d55ca58ae9da5e8476b98bd 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -49,7 +49,7 @@ Section refcell_inv.
         (* Not borrowed. *)
         &{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid)
       | Some (ν, rw, q, _) =>
-        (1.[ν] ={↑lftN,↑lft_userN}▷=∗ &{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid)) ∗
+        (1.[ν] ={↑lftN}[↑lft_userN]▷=∗ &{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid)) ∗
         (∃ q', ⌜(q + q')%Qp = 1%Qp⌝ ∗ q'.[ν]) ∗
         if rw then (* Mutably borrowed. *) True
         else       (* Immutably borrowed. *) ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1)
diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v
index c8e0f46c6c440e868f5ae5471aeca8891a37bfd9..0ba4b8eb2f27a8c33ca95e2d01eb163d3001ad26 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -34,7 +34,7 @@ Section refmut.
          ∃ (lv lrc : loc),
            &frac{κ} (λ q, l↦∗{q} [ #lv; #lrc]) ∗
            □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[α ⊓ κ]
-             ={F, F∖↑shrN}▷=∗ ty.(ty_shr) (α ⊓ κ) tid lv ∗ q.[α ⊓ κ] |}%I.
+             ={F}[F∖↑shrN]▷=∗ ty.(ty_shr) (α ⊓ κ) tid lv ∗ q.[α ⊓ κ] |}%I.
   Next Obligation.
     iIntros (???[|[[]|][|[[]|][]]]); try iIntros "[]". by iIntros "_".
   Qed.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index d793d41e8c6f67d6924e0d02b55c4849eff1a029..bffd384c00efe5a667dafce13b6e7d03da45806e 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -127,7 +127,7 @@ Section refmut_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 "INV" as (st) "(H↦lrc & H● & INV)". wp_read. wp_let. wp_op. wp_write.
-    iAssert (|={↑lftN,↑lft_userN}▷=> refcell_inv tid lrc γ β ty')%I
+    iAssert (|={↑lftN}[↑lft_userN]▷=> refcell_inv tid lrc γ β ty')%I
       with "[H↦lrc H● H◯ Hν INV]" as "INV".
     { iDestruct (own_valid_2 with "H● H◯") as
         %[[[=]|(? & [[? q'] ?] & [= <-] & Hst & INCL)]%option_included _]
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 7ed012d37380103ae901f74cf1df67e0204101ec..97fcea2a9730e1662702e7bf22430efbebb15560 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/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,↑lft_userN}▷=∗ [†ν]) ∗
+                □ (1.[ν] ={↑lftN}[↑lft_userN]▷=∗ [†ν]) ∗
                 ([†ν] ={↑lftN}=∗ &{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid)) ∗
                 ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1) ∗
                 ⌜(q + q')%Qp = 1%Qp⌝ ∗ q'.[ν]
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 932987ccea72cff27dc577ba02764cba81d3c533..cbb8f13c2e32c2ded7bc1d43b40cd47b742c3f95 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -183,7 +183,7 @@ Section rwlock_functions.
         iAssert (∃ qν ν, (qβ / 2).[β] ∗ (qν).[ν] ∗
                          ty_shr ty (β ⊓ ν) tid (lx +ₗ 1) ∗
                          own γ (◯ reading_st qν ν) ∗ rwlock_inv tid lx γ β ty ∗
-                         ((1).[ν] ={↑lftN,↑lft_userN}▷=∗ [†ν]))%I
+                         ((1).[ν] ={↑lftN}[↑lft_userN]▷=∗ [†ν]))%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/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 0967717baa141ecd3a8c855c7cee470fb566ed87..2773fa07e21c1a07ed1cb52fcaebda5ff44609dc 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -23,7 +23,7 @@ Section rwlockreadguard.
            ∃ ν q γ β, ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1) ∗
              α ⊑ β ∗ &at{β,rwlockN}(rwlock_inv tid l γ β ty) ∗
              q.[ν] ∗ own γ (◯ reading_st q ν) ∗
-             (1.[ν] ={↑lftN,↑lft_userN}▷=∗ [†ν])
+             (1.[ν] ={↑lftN}[↑lft_userN]▷=∗ [†ν])
          | _ => False
          end;
        ty_shr κ tid l :=
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index ebf0a8e75f209e7d0a892bb854b8171752e670f3..b5698df18544bce0a9909b42ad17b23ae1d4793b 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -83,7 +83,7 @@ Section rwlockreadguard_functions.
     iMod (at_bor_acc_tok with "LFT Hinv Hβ") as "[INV Hcloseβ]"; [done..|].
     iDestruct "INV" as (st') "(Hlx & >H● & Hst)".
     destruct (decide (Z_of_rwlock_st st = Z_of_rwlock_st st')) as [->|?].
-    + iAssert (|={⊤ ∖ ↑rwlockN,⊤ ∖ ↑rwlockN ∖ ↑lftN}▷=>
+    + iAssert (|={⊤ ∖ ↑rwlockN}[⊤ ∖ ↑rwlockN ∖ ↑lftN]▷=>
                (lx' ↦ #(Z_of_rwlock_st st'-1) ==∗ rwlock_inv tid lx' γ β ty))%I
         with "[H● H◯ Hx' Hν Hst H†]" as "INV".
       { iDestruct (own_valid_2 with "H● H◯") as %[[[=]| (? & st0 & [=<-] & -> & [Heq|Hle])]
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index ef2e9d2b924a6c66d9a23f3ceb3ef7ba11f6689b..aabe30e73f7ad86a30ec3900f034bfd94817e528 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -29,7 +29,7 @@ Section rwlockwriteguard.
        ty_shr κ tid l :=
          ∃ (l' : loc),
            &frac{κ} (λ q, l↦∗{q} [ #l']) ∗
-           □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[α ⊓ κ] ={F, F∖↑shrN}▷=∗
+           □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[α ⊓ κ] ={F}[F∖↑shrN]▷=∗
                ty.(ty_shr) (α ⊓ κ) tid (l' +ₗ 1) ∗ q.[α ⊓ κ] |}%I.
   Next Obligation. by iIntros (???[|[[]|][]]) "?". Qed.
   Next Obligation.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 3ac859d671f7e23250a61825fc9dcd85918f2ef6..22cfa025e8a2aaac160e041714fdd7e8a3353531 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -61,7 +61,7 @@ Section own.
          end%I;
        ty_shr κ tid l :=
          (∃ l':loc, &frac{κ}(λ q', l ↦{q'} #l') ∗
-            □ (∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[κ] ={F,F∖↑shrN}▷=∗
+            □ (∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[κ] ={F}[F∖↑shrN]▷=∗
                             ty.(ty_shr) κ tid l' ∗ q.[κ]))%I |}.
   Next Obligation. by iIntros (q ty tid [|[[]|][]]) "H". Qed.
   Next Obligation.
@@ -80,7 +80,7 @@ Section own.
     intros _ ty κ κ' tid l. iIntros "#Hκ #H".
     iDestruct "H" as (l') "[Hfb #Hvs]".
     iExists l'. iSplit. by iApply (frac_bor_shorten with "[]"). iIntros "!# *% Htok".
-    iApply (step_fupd_mask_mono F _ _ (F∖↑shrN)); [solve_ndisj..|].
+    iApply (step_fupd_mask_mono F _ (F∖↑shrN)); [solve_ndisj..|].
     iMod (lft_incl_acc with "Hκ Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
     iMod ("Hvs" with "[%] Htok") as "Hvs'"; first solve_ndisj. iModIntro. iNext.
     iMod "Hvs'" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index a84b95b423ded0750fb579ce735420f19b16cda8..d2c80811f9e57bb553f40c704235b3b888f170d6 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -17,7 +17,7 @@ Section uniq_bor.
        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' ∗ q.[κ⊓κ']
+               ={F}[F∖↑shrN]▷=∗ ty.(ty_shr) (κ⊓κ') tid l' ∗ q.[κ⊓κ']
     |}%I.
   Next Obligation. by iIntros (q ty tid [|[[]|][]]) "H". Qed.
   Next Obligation.
@@ -34,7 +34,7 @@ Section uniq_bor.
     iDestruct "H" as (l') "[Hfb Hvs]". iAssert (κ0⊓κ' ⊑ κ0⊓κ)%I as "#Hκ0".
     { iApply lft_intersect_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)); try solve_ndisj.
+    iIntros "!# * % Htok". iApply (step_fupd_mask_mono F _ (F∖↑shrN)); try solve_ndisj.
     iMod (lft_incl_acc with "Hκ0 Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
     iMod ("Hvs" with "[%] Htok") as "Hvs'"; first solve_ndisj. iModIntro. iNext.
     iMod "Hvs'" as "[#Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
diff --git a/theories/typing/util.v b/theories/typing/util.v
index ce4cb5713ca21f7ea42cb52a91b669435cb9634a..3dab3ddc3a31b41d2ffd02342ef8df8047652637 100644
--- a/theories/typing/util.v
+++ b/theories/typing/util.v
@@ -21,15 +21,15 @@ Section util.
   Lemma delay_borrow_step :
     lfeE ⊆ N → (∀ x, Persistent (Post x)) →
     lft_ctx -∗ &{κ} P -∗
-      □ (∀ x, &{κ} P -∗ Pre x -∗ Frame x ={F1 x,F2 x}▷=∗ Post x ∗ Frame x) ={N}=∗ 
-      □ (∀ x, Pre x -∗ Frame x ={F1 x,F2 x}▷=∗ Post x ∗ Frame x).
+      □ (∀ x, &{κ} P -∗ Pre x -∗ Frame x ={F1 x}[F2 x]▷=∗ Post x ∗ Frame x) ={N}=∗ 
+      □ (∀ x, Pre x -∗ Frame x ={F1 x}[F2 x]▷=∗ Post x ∗ Frame x).
    *)
 
   Lemma delay_sharing_later N κ l ty tid :
     lftE ⊆ N →
     lft_ctx -∗ &{κ}(▷ l ↦∗: ty_own ty tid) ={N}=∗
        □ ∀ (F : coPset) (q : Qp),
-       ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ (q).[κ] ={F,F ∖ ↑shrN}▷=∗ ty.(ty_shr) κ tid l ∗ (q).[κ].
+       ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ (q).[κ] ={F}[F ∖ ↑shrN]▷=∗ ty.(ty_shr) κ tid l ∗ (q).[κ].
   Proof.
     iIntros (?) "#LFT Hbor". rewrite bor_unfold_idx.
     iDestruct "Hbor" as (i) "(#Hpb&Hpbown)".
@@ -51,7 +51,7 @@ Section util.
     lftE ⊆ N →
     lft_ctx -∗ ▷ (κ'' ⊑ κ ⊓ κ') -∗ &{κ'}(&{κ}(l ↦∗: ty_own ty tid)) ={N}=∗
        □ ∀ (F : coPset) (q : Qp),
-       ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ (q).[κ''] ={F,F ∖ ↑shrN}▷=∗ ty.(ty_shr) κ'' tid l ∗ (q).[κ''].
+       ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ (q).[κ''] ={F}[F ∖ ↑shrN]▷=∗ ty.(ty_shr) κ'' tid l ∗ (q).[κ''].
   Proof.
     iIntros (?) "#LFT #Hincl Hbor". rewrite bor_unfold_idx.
     iDestruct "Hbor" as (i) "(#Hpb&Hpbown)".