diff --git a/opam b/opam
index 866ad3bd841a998800f79a6f04d5cd527fa45e88..e4b0f02eb952a8cbd6ab509cbfa04909f716d1ea 100644
--- a/opam
+++ b/opam
@@ -16,7 +16,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2020-06-19.2.6c60d47a") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2020-07-03.0.ce4c6d6b") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index cef8a16d0b60b026feb692d510e7301055556f2c..e87fcc146f97e63f6b52ccba65dbb34d6bc4bff9 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -149,7 +149,7 @@ Proof.
 Qed.
 
 Lemma bor_later `{LatBottom Lat} E κ P :
-  ↑lftN ⊆ E → ⎡lft_ctx⎤ -∗ &{κ}(▷ P) ={E,E∖↑lftN}▷=∗ &{κ}P.
+  ↑lftN ⊆ E → ⎡lft_ctx⎤ -∗ &{κ}(▷ P) ={E}[E∖↑lftN]▷=∗ &{κ}P.
 Proof.
   iIntros (?) "#LFT Hb".
   iMod (bor_acc_atomic_cons with "LFT Hb") as "[H|H]"; first done.
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 9c3fca84a4b8e9d7a0aaeba4bcc80747eccf8531..765bb4b575ab403ff2b8442234554e60b748181d 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -109,7 +109,7 @@ Module Type lifetime_sig.
   Parameter lft_dead_static : [† static] -∗ False.
 
   Parameter lft_create : ∀ `{LatBottom Lat} E, ↑lftN ⊆ E →
-    ⎡lft_ctx⎤ ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={↑lftN ∪ E0, E0}▷=∗ [†κ]).
+    ⎡lft_ctx⎤ ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={↑lftN ∪ E0}[E0]▷=∗ [†κ]).
   Parameter bor_create : ∀ `{LatBottom Lat} E κ P,
     ↑lftN ⊆ E → ⎡lft_ctx⎤ -∗ ▷ P ={E}=∗ &{κ}P ∗ ([†κ] ={E}=∗ ▷ P).
   Parameter bor_fake : ∀ `{LatBottom Lat} E κ P,
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index df30fe502a2f9267d05b0781b2576e098884d2e6..6e71e3e083f62898200ac8f005c5b74b4fbcb774 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -152,7 +152,7 @@ Proof.
 Qed.
 
 Lemma lft_create E :
-  ↑lftN ⊆ E → ⎡lft_ctx⎤ ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={↑lftN ∪ E0,E0}▷=∗ [†κ]).
+  ↑lftN ⊆ E → ⎡lft_ctx⎤ ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={↑lftN ∪ E0}[E0]▷=∗ [†κ]).
 Proof.
   iIntros (?) "#LFT".
   iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
@@ -176,7 +176,7 @@ Proof.
     iDestruct (monPred_in_intro True%I with "[//]") as (V) "[H _]".
     by rewrite -(lat_bottom_sqsubseteq V). }
   clear I A HΛ. iIntros "!# HΛ".
-  iApply (step_fupd_mask_mono (↑lftN ∪ E0) _ _ ((↑lftN ∪ E0)∖↑mgmtN)); [|done|].
+  iApply (step_fupd_mask_mono (↑lftN ∪ E0) _ ((↑lftN ∪ E0)∖↑mgmtN)); [|done|].
   { assert (↑mgmtN ## E0) by (pose proof E0_lftN_disj; solve_ndisj). set_solver. }
   iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
   { rewrite <-union_subseteq_l. solve_ndisj. }
diff --git a/theories/logic/gps.v b/theories/logic/gps.v
index ce337cab525fc21505c9bc8bef68bac90ef0c57c..68c5d13a88060aea00f9c8f6fd7fc662d7856953 100644
--- a/theories/logic/gps.v
+++ b/theories/logic/gps.v
@@ -133,7 +133,7 @@ Lemma GPS_aSP_SharedWriter_CAS_int_weak
               (∀ t'' , ⌜(t' < t'')%positive⌝ -∗
                   ▷ GPS_SWSharedWriter l t'' s'' vw γ ={E ∖ ↑N}=∗
                   (<obj> (▷ Q1 t' s' ={E ∖ ↑N}=∗ ▷ IP false l γ t' s' #vr)) ∗
-                  |={E ∖ ↑N,E'}▷=> Q t'' s'' ∗ ▷ IP true l γ t'' s'' vw))) ) ∧
+                  |={E ∖ ↑N}[E']▷=> Q t'' s'' ∗ ▷ IP true l γ t'' s'' vw))) ) ∧
         ▷ (∀ (v: lit), ⌜lit_neq vr v⌝ -∗
         <obj> ((IP false l γ t' s' #v ={E ∖ ↑N}=∗ IP false l γ t' s' #v ∗ R t' s' v) ∧
                (IP true l γ t' s' #v ={E ∖ ↑N}=∗ IP true l γ t' s' #v ∗ R t' s' v) ∧
@@ -183,7 +183,7 @@ Lemma GPS_aSP_SharedWriter_CAS_int_strong
             (∀ t'' , ⌜(t' < t'')%positive⌝ -∗ ▷ GPS_SWSharedWriter l t'' s'' vw γ -∗
               (if dropR then ▷ GPS_SWSharedReader l t'' s'' vw qs γ else True) ={E ∖ ↑N}=∗
               (<obj> (▷ Q1 t' s' ={E ∖ ↑N}=∗ ▷ IP false l γ t' s' #vr)) ∗
-              |={E ∖ ↑N,E'}▷=> Q t'' s'' ∗ ▷ IP true l γ t'' s'' vw)) ) ∧
+              |={E ∖ ↑N}[E']▷=> Q t'' s'' ∗ ▷ IP true l γ t'' s'' vw)) ) ∧
       ▷ (∀ (v: lit), ⌜lit_neq vr v⌝ -∗
         <obj> ((IP false l γ t' s' #v ={E ∖ ↑N}=∗ IP false l γ t' s' #v ∗ R t' s' v) ∧
                (IP true l γ t' s' #v ={E ∖ ↑N}=∗ IP true l γ t' s' #v ∗ R t' s' v))))%I in
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 9c695f63357f6bfb463cf2cec1829f932a3dc877..055af49659eb57060439edbfcb00828fabab66b8 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) : vProp Σ :=
     let κ' := lft_intersect_list (x.2) in
-    (∃ κ0, ⌜x.1 = κ' ⊓ κ0⌝ ∗ q.[κ0] ∗ □ (1.[κ0] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†κ0]))%I.
+    (∃ κ0, ⌜x.1 = κ' ⊓ κ0⌝ ∗ q.[κ0] ∗ □ (1.[κ0] ={↑lftN ∪ ↑histN}[↑histN]▷=∗ [†κ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 3cc26d38b6b34a14743fbc1ccf647d9d0ad911b8..c4335c6b99cbf32f779089bdefb6a94ba81e4a1f 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -34,7 +34,7 @@ Section arc.
      (*    because [weak_new] cannot prove ty_shr, even for a dead *)
      (*    lifetime. *)
      (ty.(ty_shr) ν tid (l +ₗ 2) ∨ [†ν]) ∗
-     □ (1.[ν] ={↑lftN ∪ ↑histN ∪ ↑arc_endN,↑histN}▷=∗
+     □ (1.[ν] ={↑lftN ∪ ↑histN ∪ ↑arc_endN}[↑histN]▷=∗
           [†ν] ∗ ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗ ⎡ † l…(2 + ty.(ty_size)) ⎤))%I.
 
   Global Instance arc_persist_ne tid ν γi γs γw γsw l n :
@@ -152,7 +152,7 @@ Section arc.
        ty_shr κ tid l :=
          ∃ (l' : loc), &frac{κ} (λ q, l ↦{q} #l') ∗
            □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[κ]
-             ={F, F∖↑shrN}▷=∗ q.[κ] ∗ ∃ γi γs γw γsw ν, κ ⊑ ν ∗
+             ={F}[F∖↑shrN]▷=∗ q.[κ] ∗ ∃ γi γs γw γsw ν, κ ⊑ ν ∗
                 arc_persist tid ν γi γs γw γsw l' ty ∗
                 ∃ q' ts tw, shared_arc_local l' γs γw ts tw ∗
                 &at{κ, arc_shrN}(strong_arc ts q' l' γi γs γw γsw)
@@ -291,7 +291,7 @@ Section arc.
        ty_shr κ tid l :=
          ∃ (l' : loc), &frac{κ} (λ q, l ↦{q} #l') ∗
            □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[κ]
-             ={F, F∖↑shrN}▷=∗ q.[κ] ∗ ∃ γi γs γw γsw ν,
+             ={F}[F∖↑shrN]▷=∗ q.[κ] ∗ ∃ γi γs γw γsw ν,
                 arc_persist tid ν γi γs γw γsw l' ty ∗
                 ∃ q' ts tw, shared_arc_local l' γs γw ts tw ∗
                 &at{κ, arc_shrN}(weak_arc tw q' l' γi γs γw γsw)
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index 0834d1ed0f0fba3bdab7af301675c50c39bc24cc..28f36d795e25e7055f55630a78ebbb5712bd2345 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -38,7 +38,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 a098f55a2973fd0c0d82ab7f798b3c6023045b13..e1f93314cb698e1ae0e8585b5acd52ca7fc1db28 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -86,7 +86,7 @@ Section rc.
                  because [weak_new] cannot prove ty_shr, even for a dead
                  lifetime. *)
               (ty.(ty_shr) ν tid (l +ₗ 2) ∨ [†ν]) ∗
-              □ (1.[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†ν]))%I.
+              □ (1.[ν] ={↑lftN ∪ ↑histN}[↑histN]▷=∗ [†ν]))%I.
 
   Global Instance rc_persist_persistent : Persistent (rc_persist tid ν γ l ty).
   Proof. unfold rc_persist, tc_opaque. apply _. Qed.
@@ -124,7 +124,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.
@@ -254,16 +254,16 @@ Section code.
         (((⌜strong = 1%positive⌝ ∗
            (∃ weak : Z, (l +ₗ 1) ↦ #weak ∗
              ((⌜weak = 1⌝ ∗
-               |={⊤,↑histN}▷=> ⎡† l…(2 + ty.(ty_size))⎤ ∗
+               |={⊤}[↑histN]▷=> ⎡† 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)
-                ={⊤,↑histN}▷=∗ ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗
+                ={⊤}[↑histN]▷=∗ ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗
                 ((l +ₗ 2) ↦∗: (λ vl, ⌜length vl = ty.(ty_size)⌝)
                  ={⊤}=∗ na_own tid F)))))) ∧
-           (l ↦ #0 ={⊤,↑histN}▷=∗
+           (l ↦ #0 ={⊤}[↑histN]▷=∗
              ▷ (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 77586f496d796954b40baab8b93a307cd862e125..7f441063b9ee28cc2c638dd05e65da1bd076f267 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 4a42835ef1e67a1dfaa213d80333c12a1f490b0a..81ac8abd96a065f867295e84f29c7d819dfe6808 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -14,7 +14,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 ∪ ↑histN,↑histN}▷=∗ &{α}((l +ₗ 1) ↦∗: ty_own ty tid)) ∗
+            ((1).[ν] ={↑lftN ∪ ↑histN}[↑histN]▷=∗ &{α}((l +ₗ 1) ↦∗: ty_own ty tid)) ∗
             (∃ q'', ⌜(q' + q'' = 1)%Qp⌝ ∗ q''.[ν]) ∗
             ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1).
   Proof.
@@ -161,7 +161,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 ∪ ↑histN,↑histN}▷=> refcell_inv tid lrc γ β ty')%I
+    iAssert (|={↑lftN ∪ ↑histN}[↑histN]▷=> 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 1341fca878b801c7f8d30f28dbd68006c69d465c..ec39aa1fdba40521280aa418e0d79428b9a3dfc2 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -48,7 +48,7 @@ Section refcell_inv.
         (* Not borrowed. *)
         &{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid)
       | Some (ν, rw, q, _) =>
-        (1.[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ &{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid)) ∗
+        (1.[ν] ={↑lftN ∪ ↑histN}[↑histN]▷=∗ &{α}((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 9161ac9d3c37c50df6e8baf790d5e365d8f64e4b..0f51cf44dc1a1b902ef5179bec3877ccb3993e76 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -33,7 +33,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 bc776ababd5da3b854a8fc567fafd8b3f23be5c4..7b7b7785d0e1fa67b0a95a1490caef82605077b4 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -126,7 +126,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 ∪ ↑histN,↑histN}▷=> refcell_inv tid lrc γ β ty')%I
+    iAssert (|={↑lftN ∪ ↑histN}[↑histN]▷=> 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 248132e699e00fd4560d1727dfd2cdfbfbfc1e2b..2dab818e348ecb5c5bfc8aa723c84548b6f50adc 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -178,7 +178,7 @@ Section rwlock_inv.
                   GPS_SWSharedReader l t () #0 1%Qp γ
             | Some (inr (ν, q, n)) => (* Locked for read. *)
                   GPS_SWSharedWriter l t () #(Z.pos n) γ ∗
-                  ∃ q', □ (1.[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†ν]) ∗
+                  ∃ q', □ (1.[ν] ={↑lftN ∪ ↑histN}[↑histN]▷=∗ [†ν]) ∗
                     ([†ν] ={↑lftN ∪ ↑histN}=∗ &{α}tyO) ∗
                     (□ tyS (α ⊓ ν)) ∗ ⌜(q + q')%Qp = 1%Qp⌝ ∗
                     q'.[ν] ∗
@@ -277,7 +277,7 @@ Section rwlock_inv.
                 | None => (* Not locked. *)
                       &{α}tyO
                 | Some (inr (ν, q, n)) => (* Locked for read. *)
-                      ∃ q', □ (1.[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†ν]) ∗
+                      ∃ q', □ (1.[ν] ={↑lftN ∪ ↑histN}[↑histN]▷=∗ [†ν]) ∗
                         ([†ν] ={↑lftN ∪ ↑histN}=∗ &{α}tyO) ∗
                         (□ tyS (α ⊓ ν)) ∗ ⌜(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 7acb5a20b2993aa0afd53c6b72b508b09fccefc8..227757d16aa8143552a16bdd71be88b25109cded 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -210,7 +210,7 @@ Section rwlock_functions.
           (∃ qν ν, (qν).[ν] ∗
             (□ tyS (β ⊓ ν)) ∗
             rwown γs (reading_st qν ν) ∗
-            (□ ((1).[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†ν])) ∗
+            (□ ((1).[ν] ={↑lftN ∪ ↑histN}[↑histN]▷=∗ [†ν])) ∗
             GPS_SWSharedReader lx t (() : unitProtocol) #(Z_of_rwlock_st st' + 1) qν γ))%I.
       set Q1: time → () → vProp Σ :=
         (λ t _, rwlock_interp γs β tyO tyS false lx γ t () #(Z_of_rwlock_st st'))%I.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 2f9d709e2758c1c310feed2425514e1d919c29b2..d7b5b5fdbc10fac39eeb7dd909dfe8a321c9083d 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -23,7 +23,7 @@ Section rwlockreadguard.
          | [ #(LitLoc l) ] =>
            ∃ ν q γs β, ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1) ∗
              α ⊑ β ∗ q.[ν] ∗ rwown γs (reading_st q ν) ∗
-             □ (1.[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†ν]) ∗
+             □ (1.[ν] ={↑lftN ∪ ↑histN}[↑histN]▷=∗ [†ν]) ∗
              (∃ γ tyO tyS, (∃ t n, GPS_SWSharedReader l t () #n q γ) ∗
                   rwlock_proto l γ γs β tyO tyS tid ty)
          | _ => False
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index ecd96a9751d960039344ea2fc2e1fce51d19224a..f76e7f02f3e66c0ec45c9dcc3dfad36985c6bf26 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -125,7 +125,7 @@ Section rwlockreadguard_functions.
         { rewrite /Q1 Eqst. by iIntros "!> $". }
         destruct CASE as [[??]|[[q0 ?] Eqn]]; [subst q' n|subst q'].
         - rewrite Hqrq'. iMod (rwown_update_read_dealloc_1 with "H● H◯") as "H●".
-          iApply (step_fupd_mask_mono (↑lftN ∪ ↑histN) _ _ (↑histN));
+          iApply (step_fupd_mask_mono (↑lftN ∪ ↑histN) _ (↑histN));
             [solve_ndisj|apply union_least; solve_ndisj|..].
           iMod ("H†" with "Hν") as "Hν". iIntros "!> !>". iMod "Hν".
           iMod ("Hh" with "Hν") as "Hb". iModIntro.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index fbf9044936922c08b32fc764e031de454bf5b05b..baa572274b98d8aa8392daf2e0abb9b1c8f1dc45 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -31,7 +31,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 3372eab6ff115d7d83ac1d69b166e49f3c9ce79c..0677b4332d1ae712636700caea1f2e63a4dd3b35 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -62,7 +62,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.
@@ -81,7 +81,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 522d5d808f24e53f727d0c5e2832b9062887916b..e0cde6e6f88980260c2e0e595a4dda1963222792 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -16,7 +16,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.
@@ -33,7 +33,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 092d93841a79e614e2248327506c346f64732f8d..1adf126a059a3cd792438e5b6f596eec1185335b 100644
--- a/theories/typing/util.v
+++ b/theories/typing/util.v
@@ -20,15 +20,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 (monPred_in_intro with "Hbor") as (V) "[#Hin Hbor]".
@@ -58,7 +58,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.
     iCombine "Hincl Hbor" as "Hinclbor".