diff --git a/CHANGELOG.md b/CHANGELOG.md
index 019bda96a1435f90b31dd10e848b2649af7e6cfb..14f521a0cf506aff8a227cd04b9de4ed0f9423fe 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -108,6 +108,8 @@ Coq 8.11 is no longer supported in this version of Iris.
      to ignore the new step counter.
   (by Jacques-Henri Jourdan)
 * Remove `wp_frame_wand_l`; add `wp_frame_wand` as more symmetric replacement.
+* Swap the polarity of the mask in logically atomic triples, so that it matches
+  regular `WP` masks.
 
 **Changes in `heap_lang`:**
 
diff --git a/iris/bi/lib/atomic.v b/iris/bi/lib/atomic.v
index f67fc975c6f8c9046fa3b37f0ab458da5fcbfb7b..e4dd512cb7c076cb1a28e701fd66e7412c181d0e 100644
--- a/iris/bi/lib/atomic.v
+++ b/iris/bi/lib/atomic.v
@@ -113,7 +113,7 @@ Notation "'AU' '<<' ∀ x1 .. xn , α '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'C
                         ) .. )
   )
   (at level 20, Eo, Ei, α, β, Φ at level 200, x1 binder, xn binder, y1 binder, yn binder,
-   format "'[   ' 'AU'  '<<'  ∀  x1  ..  xn ,  α  '>>'  '/' @  Eo ,  Ei  '/' '[   ' '<<'  ∃  y1  ..  yn ,  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.
+   format "'[   ' 'AU'  '<<'  ∀  x1  ..  xn ,  α  '>>'  '/' '[' @  Eo ,  Ei  ']' '/' '[   ' '<<'  ∃  y1  ..  yn ,  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.
 
 Notation "'AU' '<<' ∀ x1 .. xn , α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
   (atomic_update (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
@@ -127,7 +127,7 @@ Notation "'AU' '<<' ∀ x1 .. xn , α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :
                        λ x1, .. (λ xn, tele_app (TT:=TeleO) Φ%I) .. )
   )
   (at level 20, Eo, Ei, α, β, Φ at level 200, x1 binder, xn binder,
-   format "'[   ' 'AU'  '<<'  ∀  x1  ..  xn ,  α  '>>'  '/' @  Eo ,  Ei  '/' '[   ' '<<'  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.
+   format "'[   ' 'AU'  '<<'  ∀  x1  ..  xn ,  α  '>>'  '/' '[' @  Eo ,  Ei  ']' '/' '[   ' '<<'  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.
 
 Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
   (atomic_update (TA:=TeleO)
@@ -142,7 +142,7 @@ Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :
                                 (λ y1, .. (λ yn, Φ%I) ..))
   )
   (at level 20, Eo, Ei, α, β, Φ at level 200, y1 binder, yn binder,
-   format "'[   ' 'AU'  '<<'  α  '>>'  '/' @  Eo ,  Ei  '/' '[   ' '<<'  ∃  y1  ..  yn ,  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.
+   format "'[   ' 'AU'  '<<'  α  '>>'  '/' '[' @  Eo ,  Ei  ']' '/' '[   ' '<<'  ∃  y1  ..  yn ,  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.
 
 Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
   (atomic_update (TA:=TeleO) (TB:=TeleO) Eo Ei
@@ -151,7 +151,7 @@ Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
                  (tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) Φ%I)
   )
   (at level 20, Eo, Ei, α, β, Φ at level 200,
-   format "'[   ' 'AU'  '<<'  α  '>>'  '/' @  Eo ,  Ei  '/' '[   ' '<<'  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.
+   format "'[   ' 'AU'  '<<'  α  '>>'  '/' '[' @  Eo ,  Ei  ']' '/' '[   ' '<<'  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.
 
 (** Notation: Atomic accessors *)
 Notation "'AACC' '<<' ∀ x1 .. xn , α 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
@@ -173,7 +173,7 @@ Notation "'AACC' '<<' ∀ x1 .. xn , α 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 ..
                      ) .. )
   )
   (at level 20, Eo, Ei, α, P, β, Φ at level 200, x1 binder, xn binder, y1 binder, yn binder,
-   format "'[     ' 'AACC'  '[   ' '<<'  ∀  x1  ..  xn ,  α  '/' ABORT  P  '>>'  ']' '/' @  Eo ,  Ei  '/' '[   ' '<<'  ∃  y1  ..  yn ,  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.
+   format "'[     ' 'AACC'  '[   ' '<<'  ∀  x1  ..  xn ,  α  '/' ABORT  P  '>>'  ']' '/' '[' @  Eo ,  Ei  ']' '/' '[   ' '<<'  ∃  y1  ..  yn ,  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.
 
 Notation "'AACC' '<<' ∀ x1 .. xn , α 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
   (atomic_acc (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
@@ -188,7 +188,7 @@ Notation "'AACC' '<<' ∀ x1 .. xn , α 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM
                         λ x1, .. (λ xn, tele_app (TT:=TeleO) Φ%I) .. )
   )
   (at level 20, Eo, Ei, α, P, β, Φ at level 200, x1 binder, xn binder,
-   format "'[     ' 'AACC'  '[   ' '<<'  ∀  x1  ..  xn ,  α  '/' ABORT  P  '>>'  ']' '/' @  Eo ,  Ei  '/' '[   ' '<<'  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.
+   format "'[     ' 'AACC'  '[   ' '<<'  ∀  x1  ..  xn ,  α  '/' ABORT  P  '>>'  ']' '/' '[' @  Eo ,  Ei  ']' '/' '[   ' '<<'  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.
 
 Notation "'AACC' '<<' α 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
   (atomic_acc (TA:=TeleO)
@@ -204,7 +204,7 @@ Notation "'AACC' '<<' α 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM
                         (λ y1, .. (λ yn, Φ%I) ..))
   )
   (at level 20, Eo, Ei, α, P, β, Φ at level 200, y1 binder, yn binder,
-   format "'[     ' 'AACC'  '[   ' '<<'  α  '/' ABORT  P  '>>'  ']' '/' @  Eo ,  Ei  '/' '[   ' '<<'  ∃  y1  ..  yn ,  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.
+   format "'[     ' 'AACC'  '[   ' '<<'  α  '/' ABORT  P  '>>'  ']' '/' '[' @  Eo ,  Ei  ']' '/' '[   ' '<<'  ∃  y1  ..  yn ,  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.
 
 Notation "'AACC' '<<' α 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
   (atomic_acc (TA:=TeleO)
@@ -216,7 +216,7 @@ Notation "'AACC' '<<' α 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
                  (tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) Φ%I)
   )
   (at level 20, Eo, Ei, α, P, β, Φ at level 200,
-   format "'[     ' 'AACC'  '[   ' '<<'  α  '/' ABORT  P  '>>'  ']' '/' @  Eo ,  Ei  '/' '[   ' '<<'  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.
+   format "'[     ' 'AACC'  '[   ' '<<'  α  '/' ABORT  P  '>>'  ']' '/' '[' @  Eo ,  Ei  ']' '/' '[   ' '<<'  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.
 
 (** Lemmas about AU *)
 Section lemmas.
diff --git a/iris/program_logic/atomic.v b/iris/program_logic/atomic.v
index 02a1b3fe2f56fbb4293bec3ee7204d46d4b116db..8feb932af91cb7f2e68973dcbc18f811215a74f4 100644
--- a/iris/program_logic/atomic.v
+++ b/iris/program_logic/atomic.v
@@ -10,22 +10,24 @@ From iris.prelude Require Import options.
 example where we want it to be anything else. *)
 Definition atomic_wp `{!irisGS Λ Σ} {TA TB : tele}
   (e: expr Λ) (* expression *)
-  (Eo : coPset) (* (outer) mask *)
+  (E : coPset) (* *implementation* mask *)
   (α: TA → iProp Σ) (* atomic pre-condition *)
   (β: TA → TB → iProp Σ) (* atomic post-condition *)
   (f: TA → TB → val Λ) (* Turn the return data into the return value *)
   : iProp Σ :=
     ∀ (Φ : val Λ → iProp Σ),
-            atomic_update Eo ∅ α β (λ.. x y, Φ (f x y)) -∗
+            (* The (outer) user mask is what is left after the implementation
+            opened its things. *)
+            atomic_update (⊤∖E) ∅ α β (λ.. x y, Φ (f x y)) -∗
             WP e {{ Φ }}.
 (* Note: To add a private postcondition, use
    atomic_update α β Eo Ei (λ x y, POST x y -∗ Φ (f x y)) *)
 
-Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ Eo '<<<' ∃ y1 .. yn , β , 'RET' v '>>>'" :=
+Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ E '<<<' ∃ y1 .. yn , β , 'RET' v '>>>'" :=
   (atomic_wp (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
              (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
              e%E
-             Eo
+             E
              (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
                        λ x1, .. (λ xn, α%I) ..)
              (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
@@ -39,15 +41,15 @@ Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ Eo '<<<' ∃ y1 .. yn , β , 'RET' v
                          (λ y1, .. (λ yn, v%V) .. )
                         ) .. )
   )
-  (at level 20, Eo, α, β, v at level 200, x1 binder, xn binder, y1 binder, yn binder,
-   format "'[hv' '<<<'  ∀  x1  ..  xn ,  α  '>>>'  '/  ' e  @  Eo  '/' '[    ' '<<<'  ∃  y1  ..  yn ,  β ,  '/' 'RET'  v  '>>>' ']' ']'")
+  (at level 20, E, α, β, v at level 200, x1 binder, xn binder, y1 binder, yn binder,
+   format "'[hv' '<<<'  ∀  x1  ..  xn ,  α  '>>>'  '/  ' e  @  E  '/' '[    ' '<<<'  ∃  y1  ..  yn ,  β ,  '/' 'RET'  v  '>>>' ']' ']'")
   : bi_scope.
 
-Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ Eo '<<<' β , 'RET' v '>>>'" :=
+Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ E '<<<' β , 'RET' v '>>>'" :=
   (atomic_wp (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
              (TB:=TeleO)
              e%E
-             Eo
+             E
              (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
                        λ x1, .. (λ xn, α%I) ..)
              (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
@@ -59,15 +61,15 @@ Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ Eo '<<<' β , 'RET' v '>>>'" :=
                          tele_app (TT:=TeleO) v%V
                         ) .. )
   )
-  (at level 20, Eo, α, β, v at level 200, x1 binder, xn binder,
-   format "'[hv' '<<<'  ∀  x1  ..  xn ,  α  '>>>'  '/  ' e  @  Eo  '/' '[    ' '<<<'  β ,  '/' 'RET'  v  '>>>' ']' ']'")
+  (at level 20, E, α, β, v at level 200, x1 binder, xn binder,
+   format "'[hv' '<<<'  ∀  x1  ..  xn ,  α  '>>>'  '/  ' e  @  E  '/' '[    ' '<<<'  β ,  '/' 'RET'  v  '>>>' ']' ']'")
   : bi_scope.
 
-Notation "'<<<' α '>>>' e @ Eo '<<<' ∃ y1 .. yn , β , 'RET' v '>>>'" :=
+Notation "'<<<' α '>>>' e @ E '<<<' ∃ y1 .. yn , β , 'RET' v '>>>'" :=
   (atomic_wp (TA:=TeleO)
              (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
              e%E
-             Eo
+             E
              (tele_app (TT:=TeleO) α%I)
              (tele_app (TT:=TeleO) $
                        tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
@@ -76,21 +78,21 @@ Notation "'<<<' α '>>>' e @ Eo '<<<' ∃ y1 .. yn , β , 'RET' v '>>>'" :=
                        tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
                          (λ y1, .. (λ yn, v%V) .. ))
   )
-  (at level 20, Eo, α, β, v at level 200, y1 binder, yn binder,
-   format "'[hv' '<<<'  α  '>>>'  '/  ' e  @  Eo  '/' '[    ' '<<<'  ∃  y1  ..  yn ,  β ,  '/' 'RET'  v  '>>>' ']' ']'")
+  (at level 20, E, α, β, v at level 200, y1 binder, yn binder,
+   format "'[hv' '<<<'  α  '>>>'  '/  ' e  @  E  '/' '[    ' '<<<'  ∃  y1  ..  yn ,  β ,  '/' 'RET'  v  '>>>' ']' ']'")
   : bi_scope.
 
-Notation "'<<<' α '>>>' e @ Eo '<<<' β , 'RET' v '>>>'" :=
+Notation "'<<<' α '>>>' e @ E '<<<' β , 'RET' v '>>>'" :=
   (atomic_wp (TA:=TeleO)
              (TB:=TeleO)
              e%E
-             Eo
+             E
              (tele_app (TT:=TeleO) α%I)
              (tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) β%I)
              (tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) v%V)
   )
-  (at level 20, Eo, α, β, v at level 200,
-   format "'[hv' '<<<'  α  '>>>'  '/  ' e  @  Eo  '/' '[    ' '<<<'  β ,  '/' 'RET'  v  '>>>' ']' ']'")
+  (at level 20, E, α, β, v at level 200,
+   format "'[hv' '<<<'  α  '>>>'  '/  ' e  @  E  '/' '[    ' '<<<'  β ,  '/' 'RET'  v  '>>>' ']' ']'")
   : bi_scope.
 
 (** Theory *)
@@ -99,16 +101,9 @@ Section lemmas.
   Notation iProp := (iProp Σ).
   Implicit Types (α : TA → iProp) (β : TA → TB → iProp) (f : TA → TB → val Λ).
 
-  Lemma atomic_wp_mask_weaken e Eo1 Eo2 α β f :
-    Eo2 ⊆ Eo1 → atomic_wp e Eo1 α β f -∗ atomic_wp e Eo2 α β f.
-  Proof.
-    iIntros (HEo) "Hwp". iIntros (Φ) "AU". iApply "Hwp".
-    iApply atomic_update_mask_weaken; last done. done.
-  Qed.
-
   (* Atomic triples imply sequential triples if the precondition is laterable. *)
-  Lemma atomic_wp_seq e Eo α β f {HL : ∀.. x, Laterable (α x)} :
-    atomic_wp e Eo α β f -∗
+  Lemma atomic_wp_seq e E α β f {HL : ∀.. x, Laterable (α x)} :
+    atomic_wp e E α β f -∗
     ∀ Φ, ∀.. x, α x -∗ (∀.. y, β x y -∗ Φ (f x y)) -∗ WP e {{ Φ }}.
   Proof.
     rewrite ->tforall_forall in HL. iIntros "Hwp" (Φ x) "Hα HΦ".
@@ -120,9 +115,9 @@ Section lemmas.
 
   (** This version matches the Texan triple, i.e., with a later in front of the
   [(∀.. y, β x y -∗ Φ (f x y))]. *)
-  Lemma atomic_wp_seq_step e Eo α β f {HL : ∀.. x, Laterable (α x)} :
+  Lemma atomic_wp_seq_step e E α β f {HL : ∀.. x, Laterable (α x)} :
     TCEq (to_val e) None →
-    atomic_wp e Eo α β f -∗
+    atomic_wp e E α β f -∗
     ∀ Φ, ∀.. x, α x -∗ ▷ (∀.. y, β x y -∗ Φ (f x y)) -∗ WP e {{ Φ }}.
   Proof.
     iIntros (?) "H"; iIntros (Φ x) "Hα HΦ".
@@ -133,9 +128,9 @@ Section lemmas.
   Qed.
 
   (* Sequential triples with the empty mask for a physically atomic [e] are atomic. *)
-  Lemma atomic_seq_wp_atomic e Eo α β f `{!Atomic WeaklyAtomic e} :
+  Lemma atomic_seq_wp_atomic e E α β f `{!Atomic WeaklyAtomic e} :
     (∀ Φ, ∀.. x, α x -∗ (∀.. y, β x y -∗ Φ (f x y)) -∗ WP e @ ∅ {{ Φ }}) -∗
-    atomic_wp e Eo α β f.
+    atomic_wp e E α β f.
   Proof.
     iIntros "Hwp" (Φ) "AU". iMod "AU" as (x) "[Hα [_ Hclose]]".
     iApply ("Hwp" with "Hα"). iIntros (y) "Hβ".
@@ -145,10 +140,10 @@ Section lemmas.
 
   (** Sequential triples with a persistent precondition and no initial quantifier
   are atomic. *)
-  Lemma persistent_seq_wp_atomic e Eo (α : [tele] → iProp) (β : [tele] → TB → iProp)
+  Lemma persistent_seq_wp_atomic e E (α : [tele] → iProp) (β : [tele] → TB → iProp)
         (f : [tele] → TB → val Λ) {HP : Persistent (α [tele_arg])} :
     (∀ Φ, α [tele_arg] -∗ (∀.. y, β [tele_arg] y -∗ Φ (f [tele_arg] y)) -∗ WP e {{ Φ }}) -∗
-    atomic_wp e Eo α β f.
+    atomic_wp e E α β f.
   Proof.
     simpl in HP. iIntros "Hwp" (Φ) "HΦ". iApply fupd_wp.
     iMod ("HΦ") as "[#Hα [Hclose _]]". iMod ("Hclose" with "Hα") as "HΦ".
@@ -158,26 +153,22 @@ Section lemmas.
     rewrite ->!tele_app_bind. done.
   Qed.
 
-  (** The polarity of [Eo] is the opposite of what one might expect: if you have
-      an atomic triple with some mask, you can always *shrink* that mask. *)
-  Lemma wp_atomic_mask e Eo1 Eo2 α β f :
-    Eo2 ⊆ Eo1 →
-    atomic_wp e Eo1 α β f -∗
-    atomic_wp e Eo2 α β f.
+  Lemma atomic_wp_mask_weaken e E1 E2 α β f :
+    E1 ⊆ E2 → atomic_wp e E1 α β f -∗ atomic_wp e E2 α β f.
   Proof.
-    intros ?. iIntros "Hwp" (Φ) "AU". iApply "Hwp".
-    iApply atomic_update_mask_weaken; done.
+    iIntros (HE) "Hwp". iIntros (Φ) "AU". iApply "Hwp".
+    iApply atomic_update_mask_weaken; last done. set_solver.
   Qed.
 
   (** We can open invariants around atomic triples.
       (Just for demonstration purposes; we always use [iInv] in proofs.) *)
-  Lemma wp_atomic_inv e Eo α β f N I :
-    ↑N ⊆ Eo →
-    atomic_wp e Eo (λ.. x, ▷ I ∗ α x) (λ.. x y, ▷ I ∗ β x y) f -∗
-    inv N I -∗ atomic_wp e (Eo ∖ ↑N) α β f.
+  Lemma atomic_wp_inv e E α β f N I :
+    ↑N ⊆ E →
+    atomic_wp e (E ∖ ↑N) (λ.. x, ▷ I ∗ α x) (λ.. x y, ▷ I ∗ β x y) f -∗
+    inv N I -∗ atomic_wp e E α β f.
   Proof.
     intros ?. iIntros "Hwp #Hinv" (Φ) "AU". iApply "Hwp". iAuIntro.
-    iInv N as "HI". iApply (aacc_aupd with "AU"); first done.
+    iInv N as "HI". iApply (aacc_aupd with "AU"); first solve_ndisj.
     iIntros (x) "Hα". iAaccIntro with "[HI Hα]"; rewrite ->!tele_app_bind; first by iFrame.
     - (* abort *)
       iIntros "[HI $]". by eauto with iFrame.
diff --git a/iris_heap_lang/lib/atomic_heap.v b/iris_heap_lang/lib/atomic_heap.v
index 302215a8af72c74b5707bd6bbcbae67d0db62c2b..af057db21b019cb21539a38ee516eae530f645c0 100644
--- a/iris_heap_lang/lib/atomic_heap.v
+++ b/iris_heap_lang/lib/atomic_heap.v
@@ -29,9 +29,9 @@ Class atomic_heap {Σ} `{!heapGS Σ} := AtomicHeap {
   free_spec (l : loc) (v : val) :
     {{{ mapsto l (DfracOwn 1) v }}} free #l {{{ l, RET #l; True }}};
   load_spec (l : loc) :
-    ⊢ <<< ∀ (v : val) q, mapsto l q v >>> load #l @ ⊤ <<< mapsto l q v, RET v >>>;
+    ⊢ <<< ∀ (v : val) q, mapsto l q v >>> load #l @ ∅ <<< mapsto l q v, RET v >>>;
   store_spec (l : loc) (w : val) :
-    ⊢ <<< ∀ v, mapsto l (DfracOwn 1) v >>> store #l w @ ⊤
+    ⊢ <<< ∀ v, mapsto l (DfracOwn 1) v >>> store #l w @ ∅
       <<< mapsto l (DfracOwn 1) w, RET #() >>>;
   (* This spec is slightly weaker than it could be: It is sufficient for [w1]
   *or* [v] to be unboxed.  However, by writing it this way the [val_is_unboxed]
@@ -41,7 +41,7 @@ Class atomic_heap {Σ} `{!heapGS Σ} := AtomicHeap {
   [destruct (decide (a = b))] and it will simplify in both places. *)
   cmpxchg_spec (l : loc) (w1 w2 : val) :
     val_is_unboxed w1 →
-    ⊢ <<< ∀ v, mapsto l (DfracOwn 1) v >>> cmpxchg #l w1 w2 @ ⊤
+    ⊢ <<< ∀ v, mapsto l (DfracOwn 1) v >>> cmpxchg #l w1 w2 @ ∅
       <<< if decide (v = w1) then mapsto l (DfracOwn 1) w2 else mapsto l (DfracOwn 1) v,
         RET (v, #if decide (v = w1) then true else false) >>>;
 }.
@@ -75,7 +75,7 @@ Section derived.
 
   Lemma cas_spec (l : loc) (w1 w2 : val) :
     val_is_unboxed w1 →
-    ⊢ <<< ∀ v, mapsto l (DfracOwn 1) v >>> CAS #l w1 w2 @ ⊤
+    ⊢ <<< ∀ v, mapsto l (DfracOwn 1) v >>> CAS #l w1 w2 @ ∅
     <<< if decide (v = w1) then mapsto l (DfracOwn 1) w2 else mapsto l (DfracOwn 1) v,
         RET #if decide (v = w1) then true else false >>>.
   Proof.
@@ -114,7 +114,7 @@ Section proof.
   Qed.
 
   Lemma primitive_load_spec (l : loc) :
-    ⊢ <<< ∀ (v : val) q, l ↦{q} v >>> primitive_load #l @ ⊤
+    ⊢ <<< ∀ (v : val) q, l ↦{q} v >>> primitive_load #l @ ∅
     <<< l ↦{q} v, RET v >>>.
   Proof.
     iIntros (Φ) "AU". wp_lam.
@@ -123,7 +123,7 @@ Section proof.
   Qed.
 
   Lemma primitive_store_spec (l : loc) (w : val) :
-    ⊢ <<< ∀ v, l ↦ v >>> primitive_store #l w @ ⊤
+    ⊢ <<< ∀ v, l ↦ v >>> primitive_store #l w @ ∅
     <<< l ↦ w, RET #() >>>.
   Proof.
     iIntros (Φ) "AU". wp_lam. wp_let.
@@ -134,7 +134,7 @@ Section proof.
   Lemma primitive_cmpxchg_spec (l : loc) (w1 w2 : val) :
     val_is_unboxed w1 →
     ⊢ <<< ∀ (v : val), l ↦ v >>>
-      primitive_cmpxchg #l w1 w2 @ ⊤
+      primitive_cmpxchg #l w1 w2 @ ∅
     <<< if decide (v = w1) then l ↦ w2 else l ↦ v,
         RET (v, #if decide (v = w1) then true else false) >>>.
   Proof.
diff --git a/iris_heap_lang/lib/increment.v b/iris_heap_lang/lib/increment.v
index bf82e9b843e54dcc8dc1cfe15303424a5fd15f44..3f166ca57fed2443af255856593069632c0e652b 100644
--- a/iris_heap_lang/lib/increment.v
+++ b/iris_heap_lang/lib/increment.v
@@ -21,7 +21,7 @@ Section increment_physical.
          else "incr" "l".
 
   Lemma incr_phy_spec (l: loc) :
-    ⊢ <<< ∀ (v : Z), l ↦ #v >>> incr_phy #l @ ⊤ <<< l ↦ #(v + 1), RET #v >>>.
+    ⊢ <<< ∀ (v : Z), l ↦ #v >>> incr_phy #l @ ∅ <<< l ↦ #(v + 1), RET #v >>>.
   Proof.
     iIntros (Φ) "AU". iLöb as "IH". wp_lam.
     wp_bind (!_)%E. iMod "AU" as (v) "[Hl [Hclose _]]".
@@ -52,7 +52,7 @@ Section increment.
   (** A proof of the incr specification that unfolds the definition of atomic
       accessors.  This is the style that most logically atomic proofs take. *)
   Lemma incr_spec_direct (l: loc) :
-    ⊢ <<< ∀ (v : Z), l ↦ #v >>> incr #l @ ⊤ <<< l ↦ #(v + 1), RET #v >>>.
+    ⊢ <<< ∀ (v : Z), l ↦ #v >>> incr #l @ ∅ <<< l ↦ #(v + 1), RET #v >>>.
   Proof.
     iIntros (Φ) "AU". iLöb as "IH". wp_lam.
     awp_apply load_spec.
@@ -91,7 +91,7 @@ Section increment.
       prove are in 1:1 correspondence; most logically atomic proofs will not be
       able to use them. *)
   Lemma incr_spec (l: loc) :
-    ⊢ <<< ∀ (v : Z), l ↦ #v >>> incr #l @ ⊤ <<< l ↦ #(v + 1), RET #v >>>.
+    ⊢ <<< ∀ (v : Z), l ↦ #v >>> incr #l @ ∅ <<< l ↦ #(v + 1), RET #v >>>.
   Proof.
     iIntros (Φ) "AU". iLöb as "IH". wp_lam.
     awp_apply load_spec.
@@ -126,7 +126,7 @@ Section increment.
   Lemma weak_incr_spec (l: loc) (v : Z) :
     l ↦{#1/2} #v -∗
     <<< ∀ (v' : Z), l ↦{#1/2} #v' >>>
-      weak_incr #l @ ⊤
+      weak_incr #l @ ∅
     <<< ⌜v = v'⌝ ∗ l ↦ #(v + 1), RET #v >>>.
   Proof.
     iIntros "Hl" (Φ) "AU". wp_lam.
diff --git a/tests/atomic.ref b/tests/atomic.ref
index 8a8f1b5adf8d0d99c245294df51712e330cf1edf..bd5518b0b7d3fbd25928c5f94bd4e4d01009c6a5 100644
--- a/tests/atomic.ref
+++ b/tests/atomic.ref
@@ -9,8 +9,8 @@
   ============================
   "Hl" : l ↦ v
   --------------------------------------∗
-  AACC << ∀ (v0 : val) (q : dfrac), l ↦{q} v0 ABORT l ↦ v >> @ ⊤, ∅
-       << l ↦{q} v0, COMM Q -∗ Q >>
+  AACC << ∀ (v0 : val) (q : dfrac), l ↦{q} v0 ABORT l ↦ v >> 
+       @ ⊤ ∖ ∅, ∅ << l ↦{q} v0, COMM Q -∗ Q >>
   
 "non_laterable"
      : string
@@ -24,8 +24,8 @@
   ============================
   "HP" : â–· P
   --------------------------------------∗
-  AACC << ∀ (v : val) (q : dfrac), l ↦{q} v ABORT ▷ P >> @ ⊤, ∅
-       << l ↦{q} v, COMM True >>
+  AACC << ∀ (v : val) (q : dfrac), l ↦{q} v ABORT ▷ P >> 
+       @ ⊤ ∖ ∅, ∅ << l ↦{q} v, COMM True >>
   
 1 goal
   
@@ -37,8 +37,8 @@
   ============================
   "HP" : â–· P
   --------------------------------------∗
-  AACC << ∀ (v : val) (q : dfrac), l ↦{q} v ABORT ▷ P >> @ ⊤, ∅
-       << l ↦{q} v, COMM True >>
+  AACC << ∀ (v : val) (q : dfrac), l ↦{q} v ABORT ▷ P >> 
+       @ ⊤ ∖ ∅, ∅ << l ↦{q} v, COMM True >>
   
 "printing"
      : string
@@ -48,7 +48,7 @@
   heapGS0 : heapGS Σ
   P : val → iProp Σ
   ============================
-  ⊢ <<< ∀ x : val, P x >>> code @ ⊤ <<< ∃ y : val, P y, RET #() >>>
+  ⊢ <<< ∀ x : val, P x >>> code @ ∅ <<< ∃ y : val, P y, RET #() >>>
 1 goal
   
   Σ : gFunctors
@@ -56,7 +56,7 @@
   P : val → iProp Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << ∀ x : val, P x >> @ ⊤, ∅ << ∃ y : val, P y, COMM Φ #() >>
+  "AU" : AU << ∀ x : val, P x >> @ ⊤ ∖ ∅, ∅ << ∃ y : val, P y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -68,9 +68,9 @@
   Φ : language.val heap_lang → iProp Σ
   ============================
   _ : AACC << ∀ x : val, P x
-              ABORT AU << ∀ x : val, P x >> @ ⊤, ∅
-                       << ∃ y : val, P y, COMM Φ #() >> >> @ ⊤, ∅
-           << ∃ y : val, P y, COMM Φ #() >>
+              ABORT AU << ∀ x : val, P x >> @ ⊤ ∖ ∅, ∅ 
+                       << ∃ y : val, P y, COMM Φ #() >> >> 
+           @ ⊤ ∖ ∅, ∅ << ∃ y : val, P y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -80,7 +80,7 @@
   heapGS0 : heapGS Σ
   l : loc
   ============================
-  ⊢ <<< ∀ x : val, l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>
+  ⊢ <<< ∀ x : val, l ↦ x >>> code @ ∅ <<< l ↦ x, RET #() >>>
 1 goal
   
   Σ : gFunctors
@@ -88,7 +88,7 @@
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Φ #() >>
+  "AU" : AU << ∀ x : val, l ↦ x >> @ ⊤ ∖ ∅, ∅ << l ↦ x, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -100,8 +100,9 @@
   Φ : language.val heap_lang → iProp Σ
   ============================
   _ : AACC << ∀ x : val, l ↦ x
-              ABORT AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Φ #() >> >> 
-           @ ⊤, ∅ << l ↦ x, COMM Φ #() >>
+              ABORT AU << ∀ x : val, l ↦ x >> @ ⊤ ∖ ∅, ∅ 
+                       << l ↦ x, COMM Φ #() >> >> 
+           @ ⊤ ∖ ∅, ∅ << l ↦ x, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -111,7 +112,7 @@
   heapGS0 : heapGS Σ
   l : loc
   ============================
-  ⊢ <<< l ↦ #() >>> code @ ⊤ <<< ∃ y : val, l ↦ y, RET #() >>>
+  ⊢ <<< l ↦ #() >>> code @ ∅ <<< ∃ y : val, l ↦ y, RET #() >>>
 1 goal
   
   Σ : gFunctors
@@ -119,7 +120,7 @@
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << l ↦ #() >> @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
+  "AU" : AU << l ↦ #() >> @ ⊤ ∖ ∅, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -131,9 +132,9 @@
   Φ : language.val heap_lang → iProp Σ
   ============================
   _ : AACC << l ↦ #()
-              ABORT AU << l ↦ #() >> @ ⊤, ∅
-                       << ∃ y : val, l ↦ y, COMM Φ #() >> >> @ ⊤, ∅
-           << ∃ y : val, l ↦ y, COMM Φ #() >>
+              ABORT AU << l ↦ #() >> @ ⊤ ∖ ∅, ∅ 
+                       << ∃ y : val, l ↦ y, COMM Φ #() >> >> 
+           @ ⊤ ∖ ∅, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -143,7 +144,7 @@
   heapGS0 : heapGS Σ
   l : loc
   ============================
-  ⊢ <<< l ↦ #() >>> code @ ⊤ <<< l ↦ #(), RET #() >>>
+  ⊢ <<< l ↦ #() >>> code @ ∅ <<< l ↦ #(), RET #() >>>
 1 goal
   
   Σ : gFunctors
@@ -151,7 +152,7 @@
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Φ #() >>
+  "AU" : AU << l ↦ #() >> @ ⊤ ∖ ∅, ∅ << l ↦ #(), COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -163,8 +164,8 @@
   Φ : language.val heap_lang → iProp Σ
   ============================
   _ : AACC << l ↦ #()
-              ABORT AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Φ #() >> >> 
-           @ ⊤, ∅ << l ↦ #(), COMM Φ #() >>
+              ABORT AU << l ↦ #() >> @ ⊤ ∖ ∅, ∅ << l ↦ #(), COMM Φ #() >> >> 
+           @ ⊤ ∖ ∅, ∅ << l ↦ #(), COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -177,7 +178,7 @@
   l : loc
   ============================
   ⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x >>>
-      code @ ⊤
+      code @ ∅
     <<< ∃ y : val, l ↦ y, RET #() >>>
 1 goal
   
@@ -186,7 +187,7 @@
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x >> @ ⊤, ∅
+  "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x >> @ ⊤ ∖ ∅, ∅ 
             << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
@@ -198,7 +199,7 @@
   l : loc
   ============================
   ⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
-      code @ ⊤
+      code @ ∅
     <<< ∃ y : val, l ↦ y, RET #() >>>
 1 goal
   
@@ -208,7 +209,7 @@
   Φ : language.val heap_lang → iProp Σ
   ============================
   "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
-            @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
+            @ ⊤ ∖ ∅, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -219,7 +220,7 @@
   l : loc
   ============================
   ⊢ <<< ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
-      code @ ⊤
+      code @ ∅
     <<< ∃ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
         RET #() >>>
 1 goal
@@ -229,7 +230,8 @@
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : AU << ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
+  _ : AU << ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> 
+         @ ⊤ ∖ ∅, ∅ 
          << ∃ yyyy : val, l ↦ yyyy
                           ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
             COMM Φ #() >>
@@ -243,7 +245,7 @@
   l : loc
   ============================
   ⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
-      code @ ⊤
+      code @ ∅
     <<< l ↦ x, RET #() >>>
 1 goal
   
@@ -252,8 +254,8 @@
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
-            << l ↦ x, COMM Φ #() >>
+  "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> 
+            @ ⊤ ∖ ∅, ∅ << l ↦ x, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -265,7 +267,7 @@
   x : val
   ============================
   ⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
-      code @ ⊤
+      code @ ∅
     <<< ∃ y : val, l ↦ y, RET #() >>>
 1 goal
   
@@ -275,8 +277,8 @@
   x : val
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
-            << ∃ y : val, l ↦ y, COMM Φ #() >>
+  "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> 
+            @ ⊤ ∖ ∅, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -288,7 +290,7 @@
   x : val
   ============================
   ⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
-      code @ ⊤
+      code @ ∅
     <<< l ↦ #(), RET #() >>>
 1 goal
   
@@ -298,8 +300,8 @@
   x : val
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
-            << l ↦ #(), COMM Φ #() >>
+  "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> 
+            @ ⊤ ∖ ∅, ∅ << l ↦ #(), COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -311,7 +313,7 @@
   xx, yyyy : val
   ============================
   ⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
-      code @ ⊤
+      code @ ∅
     <<< l ↦ yyyy, RET #() >>>
 1 goal
   
@@ -322,7 +324,7 @@
   Φ : language.val heap_lang → iProp Σ
   ============================
   "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
-            @ ⊤, ∅ << l ↦ yyyy, COMM Φ #() >>
+            @ ⊤ ∖ ∅, ∅ << l ↦ yyyy, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -334,7 +336,7 @@
   xx, yyyy : val
   ============================
   ⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
-      code @ ⊤
+      code @ ∅
     <<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
         RET #() >>>
 1 goal
@@ -345,7 +347,7 @@
   xx, yyyy : val
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
+  "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤ ∖ ∅, ∅ 
             << l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
                COMM Φ #() >>
   --------------------------------------∗
@@ -363,7 +365,7 @@
   "AU" : ∃ x : val,
            P x
            ∗ (P x
-              ={∅,⊤}=∗ AU << ∀ x0 : val, P x0 >> @ ⊤, ∅
+              ={∅,⊤}=∗ AU << ∀ x0 : val, P x0 >> @ ⊤ ∖ ∅, ∅ 
                           << ∃ y : val, P y, COMM Φ #() >>)
              ∧ (∀ x0 : val, P x0 ={∅,⊤}=∗ Φ #())
   --------------------------------------∗
diff --git a/tests/atomic.v b/tests/atomic.v
index 02f88fa3d0b6537389a5d5ca8092ad0d4e32992a..b36f9b636a3fddd6b63eefc4b89009301d4a1bc7 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -42,28 +42,28 @@ Section printing.
   Definition code : expr := #().
 
   Lemma print_both_quant (P : val → iProp Σ) :
-    ⊢ <<< ∀ x, P x >>> code @ ⊤ <<< ∃ y, P y, RET #() >>>.
+    ⊢ <<< ∀ x, P x >>> code @ ∅ <<< ∃ y, P y, RET #() >>>.
   Proof.
     Show. iIntros (Φ) "AU". Show.
     iPoseProof (aupd_aacc with "AU") as "?". Show.
   Abort.
 
   Lemma print_first_quant l :
-    ⊢ <<< ∀ x, l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>.
+    ⊢ <<< ∀ x, l ↦ x >>> code @ ∅ <<< l ↦ x, RET #() >>>.
   Proof.
     Show. iIntros (Φ) "AU". Show.
     iPoseProof (aupd_aacc with "AU") as "?". Show.
   Abort.
 
   Lemma print_second_quant l :
-    ⊢ <<< l ↦ #() >>> code @ ⊤ <<< ∃ y, l ↦ y, RET #() >>>.
+    ⊢ <<< l ↦ #() >>> code @ ∅ <<< ∃ y, l ↦ y, RET #() >>>.
   Proof.
     Show. iIntros (Φ) "AU". Show.
     iPoseProof (aupd_aacc with "AU") as "?". Show.
   Abort.
 
   Lemma print_no_quant l :
-    ⊢ <<< l ↦ #() >>> code @ ⊤ <<< l ↦ #(), RET #() >>>.
+    ⊢ <<< l ↦ #() >>> code @ ∅ <<< l ↦ #(), RET #() >>>.
   Proof.
     Show. iIntros (Φ) "AU". Show.
     iPoseProof (aupd_aacc with "AU") as "?". Show.
@@ -72,49 +72,49 @@ Section printing.
   Check "Now come the long pre/post tests".
 
   Lemma print_both_quant_long l :
-    ⊢ <<< ∀ x, l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y, l ↦ y, RET #() >>>.
+    ⊢ <<< ∀ x, l ↦ x ∗ l ↦ x >>> code @ ∅ <<< ∃ y, l ↦ y, RET #() >>>.
   Proof.
     Show. iIntros (Φ) "AU". Show.
   Abort.
 
   Lemma print_both_quant_longpre l :
-    ⊢ <<< ∀ x, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y, l ↦ y, RET #() >>>.
+    ⊢ <<< ∀ x, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ∅ <<< ∃ y, l ↦ y, RET #() >>>.
   Proof.
     Show. iIntros (Φ) "AU". Show.
   Abort.
 
   Lemma print_both_quant_longpost l :
-    ⊢ <<< ∀ xx, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> code @ ⊤ <<< ∃ yyyy, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx, RET #() >>>.
+    ⊢ <<< ∀ xx, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> code @ ∅ <<< ∃ yyyy, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx, RET #() >>>.
   Proof.
     Show. iIntros (Φ) "?". Show.
   Abort.
 
   Lemma print_first_quant_long l :
-    ⊢ <<< ∀ x, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>.
+    ⊢ <<< ∀ x, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ∅ <<< l ↦ x, RET #() >>>.
   Proof.
     Show. iIntros (Φ) "AU". Show.
   Abort.
 
   Lemma print_second_quant_long l x :
-    ⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y, l ↦ y, RET #() >>>.
+    ⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ∅ <<< ∃ y, l ↦ y, RET #() >>>.
   Proof.
     Show. iIntros (Φ) "AU". Show.
   Abort.
 
   Lemma print_no_quant_long l x :
-    ⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< l ↦ #(), RET #() >>>.
+    ⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ∅ <<< l ↦ #(), RET #() >>>.
   Proof.
     Show. iIntros (Φ) "AU". Show.
   Abort.
 
   Lemma print_no_quant_longpre l xx yyyy :
-    ⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> code @ ⊤ <<< l ↦ yyyy, RET #() >>>.
+    ⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> code @ ∅ <<< l ↦ yyyy, RET #() >>>.
   Proof.
     Show. iIntros (Φ) "AU". Show.
   Abort.
 
   Lemma print_no_quant_longpost l xx yyyy :
-    ⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> code @ ⊤ <<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx, RET #() >>>.
+    ⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> code @ ∅ <<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx, RET #() >>>.
   Proof.
     Show. iIntros (Φ) "AU". Show.
   Abort.
@@ -122,7 +122,7 @@ Section printing.
   Check "Prettification".
 
   Lemma iMod_prettify (P : val → iProp Σ) :
-    ⊢ <<< ∀ x, P x >>> !#0 @ ⊤ <<< ∃ y, P y, RET #() >>>.
+    ⊢ <<< ∀ x, P x >>> !#0 @ ∅ <<< ∃ y, P y, RET #() >>>.
   Proof.
     iIntros (Φ) "AU". iMod "AU". Show.
   Abort.