diff --git a/CHANGELOG.md b/CHANGELOG.md
index 23cd9f4b3a88664500314619675d8478316c3b55..2fe145928e6a918fc85eeb37a85cc93be2420881 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -20,6 +20,8 @@ Changes in and extensions of the theory:
 * [#] The Löb rule is now a derived rule; it follows from later-intro, later
   being contractive and the fact that we can take fixpoints of contractive
   functions.
+* [#] Add atomic updates and logically atomic triples, including tactic support.
+  See `heap_lang/lib/increment.v` for an example.
 
 Changes in Coq:
 
diff --git a/tests/atomic.ref b/tests/atomic.ref
new file mode 100644
index 0000000000000000000000000000000000000000..864ff13700f6a594c1fc9049be4ba2fd06b537a5
--- /dev/null
+++ b/tests/atomic.ref
@@ -0,0 +1,340 @@
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  P : val → iProp Σ
+  ============================
+  <<< ∀ x : val, P x >>> code @ ⊤ <<< ∃ y : val, P y, RET #() >>>
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  P : val → iProp Σ
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  "AU" : AU << ∀ x : val, P x >> @ ⊤, ∅ << ∃ y : val, P y, COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  P : val → iProp Σ
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  _ : AACC << ∀ x : val, P x
+              ABORT AU << ∀ x : val, P x >> @ ⊤, ∅
+                       << ∃ y : val, P y, COMM Q -∗ Φ #() >> >> @ ⊤, ∅
+           << ∃ y : val, P y, COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  ============================
+  <<< ∀ x : val, l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  "AU" : AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  _ : AACC << ∀ x : val, l ↦ x
+              ABORT AU << ∀ x : val, l ↦ x >> @ ⊤, ∅
+                       << l ↦ x, COMM Q -∗ Φ #() >> >> @ ⊤, ∅
+           << l ↦ x, COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  ============================
+  <<< l ↦ #() >>> code @ ⊤ <<< ∃ y : val, l ↦ y, RET #() >>>
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  "AU" : AU << l ↦ #() >> @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  _ : AACC << l ↦ #()
+              ABORT AU << l ↦ #() >> @ ⊤, ∅
+                       << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >> >> @ ⊤, ∅
+           << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  ============================
+  <<< l ↦ #() >>> code @ ⊤ <<< l ↦ #(), RET #() >>>
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  "AU" : AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  _ : AACC << l ↦ #()
+              ABORT AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Q -∗ Φ #() >> >> 
+           @ ⊤, ∅ << l ↦ #(), COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+"Now come the long pre/post tests"
+     : string
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  ============================
+  <<< ∀ x : val, l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y : val, l ↦ y, RET #() >>>
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x >> @ ⊤, ∅
+            << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  ============================
+  <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
+    code @ ⊤
+  <<< ∃ y : val, l ↦ y, RET #() >>>
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
+            @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  ============================
+  <<< ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
+    code @ ⊤
+  <<< ∃ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
+      RET #() >>>
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  _ : AU << ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
+         << ∃ yyyy : val, l ↦ yyyy
+                          ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
+            COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  ============================
+  <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
+    code @ ⊤
+  <<< l ↦ x, RET #() >>>
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
+            << l ↦ x, COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  x : val
+  ============================
+  <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
+    code @ ⊤
+  <<< ∃ y : val, l ↦ y, RET #() >>>
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  x : val
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
+            << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  x : val
+  ============================
+  <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
+    code @ ⊤
+  <<< l ↦ #(), RET #() >>>
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  x : val
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
+            << l ↦ #(), COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  xx, yyyy : val
+  ============================
+  <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
+    code @ ⊤
+  <<< l ↦ yyyy, RET #() >>>
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  xx, yyyy : val
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
+            @ ⊤, ∅ << l ↦ yyyy, COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  xx, yyyy : val
+  ============================
+  <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
+    code @ ⊤
+  <<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
+      RET #() >>>
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  xx, yyyy : val
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
+            << l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
+               COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
diff --git a/tests/atomic.v b/tests/atomic.v
new file mode 100644
index 0000000000000000000000000000000000000000..87efeb553794d71993524d191bd6af104b71d721
--- /dev/null
+++ b/tests/atomic.v
@@ -0,0 +1,91 @@
+From iris.heap_lang Require Export lifting notation.
+From iris.program_logic Require Export atomic.
+From iris.proofmode Require Import tactics.
+From iris.heap_lang Require Import proofmode notation.
+Set Default Proof Using "Type".
+
+(* Test if AWP and the AU obtained from AWP print. *)
+Section printing.
+  Context `{!heapG Σ}.
+
+  Definition code : expr := #().
+
+  Lemma print_both_quant (P : val → iProp Σ) :
+    <<< ∀ x, P x >>> code @ ⊤ <<< ∃ y, P y, RET #() >>>.
+  Proof.
+    Show. iIntros (Q Φ) "? AU". Show.
+    iPoseProof (aupd_aacc with "AU") as "?". Show.
+  Abort.
+
+  Lemma print_first_quant l :
+    <<< ∀ x, l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>.
+  Proof.
+    Show. iIntros (Q Φ) "? AU". Show.
+    iPoseProof (aupd_aacc with "AU") as "?". Show.
+  Abort.
+
+  Lemma print_second_quant l :
+    <<< l ↦ #() >>> code @ ⊤ <<< ∃ y, l ↦ y, RET #() >>>.
+  Proof.
+    Show. iIntros (Q Φ) "? AU". Show.
+    iPoseProof (aupd_aacc with "AU") as "?". Show.
+  Abort.
+
+  Lemma print_no_quant l :
+    <<< l ↦ #() >>> code @ ⊤ <<< l ↦ #(), RET #() >>>.
+  Proof.
+    Show. iIntros (Q Φ) "? AU". Show.
+    iPoseProof (aupd_aacc with "AU") as "?". Show.
+  Abort.
+
+  Check "Now come the long pre/post tests".
+
+  Lemma print_both_quant_long l :
+    <<< ∀ x, l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y, l ↦ y, RET #() >>>.
+  Proof.
+    Show. iIntros (Q Φ) "? 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 #() >>>.
+  Proof.
+    Show. iIntros (Q Φ) "? 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 #() >>>.
+  Proof.
+    Show. iIntros (Q Φ) "? ?". Show.
+  Abort.
+
+  Lemma print_first_quant_long l :
+    <<< ∀ x, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>.
+  Proof.
+    Show. iIntros (Q Φ) "? 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 #() >>>.
+  Proof.
+    Show. iIntros (Q Φ) "? 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 #() >>>.
+  Proof.
+    Show. iIntros (Q Φ) "? 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 #() >>>.
+  Proof.
+    Show. iIntros (Q Φ) "? 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 #() >>>.
+  Proof.
+    Show. iIntros (Q Φ) "? AU". Show.
+  Abort.
+
+End printing.
diff --git a/theories/bi/lib/atomic.v b/theories/bi/lib/atomic.v
index 09b9ec49ce2c4b107f3732810cc774f7843df175..59df84626c95f725c2a6e0afd0dc56e49c16a8ea 100644
--- a/theories/bi/lib/atomic.v
+++ b/theories/bi/lib/atomic.v
@@ -1,5 +1,5 @@
-From iris.bi Require Export bi updates.
-From iris.bi.lib Require Import fixpoint laterable.
+From iris.bi Require Export bi updates laterable.
+From iris.bi.lib Require Import fixpoint.
 From stdpp Require Import coPset namespaces.
 From iris.proofmode Require Import coq_tactics tactics reduction.
 Set Default Proof Using "Type".
@@ -9,24 +9,24 @@ Local Tactic Notation "iSplitWith" constr(H) :=
   iApply (bi.and_parallel with H); iSplit; iIntros H.
 
 Section definition.
-  Context `{BiFUpd PROP} {A B : Type}.
+  Context `{BiFUpd PROP} {TA TB : tele}.
   Implicit Types
-    (Eo Em Ei : coPset) (* outside/module/inner masks *)
-    (α : A → PROP) (* atomic pre-condition *)
+    (Eo Ei : coPset) (* outer/inner masks *)
+    (α : TA → PROP) (* atomic pre-condition *)
     (P : PROP) (* abortion condition *)
-    (β : A → B → PROP) (* atomic post-condition *)
-    (Φ : A → B → PROP) (* post-condition *)
+    (β : TA → TB → PROP) (* atomic post-condition *)
+    (Φ : TA → TB → PROP) (* post-condition *)
   .
 
   (** atomic_acc as the "introduction form" of atomic updates: An accessor
       that can be aborted back to [P]. *)
   Definition atomic_acc Eo Ei α P β Φ : PROP :=
-    (|={Eo, Ei}=> ∃ x, α x ∗
-          ((α x ={Ei, Eo}=∗ P) ∧ (∀ y, β x y ={Ei, Eo}=∗ Φ x y))
+    (|={Eo, Ei}=> ∃.. x, α x ∗
+          ((α x ={Ei, Eo}=∗ P) ∧ (∀.. y, β x y ={Ei, Eo}=∗ Φ x y))
     )%I.
 
   Lemma atomic_acc_wand Eo Ei α P1 P2 β Φ1 Φ2 :
-    ((P1 -∗ P2) ∧ (∀ x y, Φ1 x y -∗ Φ2 x y)) -∗
+    ((P1 -∗ P2) ∧ (∀.. x y, Φ1 x y -∗ Φ2 x y)) -∗
     (atomic_acc Eo Ei α P1 β Φ1 -∗ atomic_acc Eo Ei α P2 β Φ2).
   Proof.
     iIntros "HP12 AS". iMod "AS" as (x) "[Hα Hclose]".
@@ -37,8 +37,8 @@ Section definition.
       iApply "HP12". iApply "Hclose". done.
   Qed.
 
-  Lemma atomic_acc_mask Eo Em α P β Φ :
-    atomic_acc Eo (Eo∖Em) α P β Φ ⊣⊢ ∀ E, ⌜Eo ⊆ E⌝ → atomic_acc E (E∖Em) α P β Φ.
+  Lemma atomic_acc_mask Eo Ed α P β Φ :
+    atomic_acc Eo (Eo∖Ed) α P β Φ ⊣⊢ ∀ E, ⌜Eo ⊆ E⌝ → atomic_acc E (E∖Ed) α P β Φ.
   Proof.
     iSplit; last first.
     { iIntros "Hstep". iApply ("Hstep" with "[% //]"). }
@@ -51,22 +51,32 @@ Section definition.
     - iIntros (y) "Hβ". iApply "Hclose'". iApply "Hclose". done.
   Qed.
 
+  Lemma atomic_acc_mask_weaken Eo1 Eo2 Ei α P β Φ :
+    Eo1 ⊆ Eo2 →
+    atomic_acc Eo1 Ei α P β Φ -∗ atomic_acc Eo2 Ei α P β Φ.
+  Proof.
+    iIntros (HE) "Hstep".
+    iMod fupd_intro_mask' as "Hclose1"; first done.
+    iMod "Hstep" as (x) "[Hα Hclose2]". iIntros "!>". iExists x.
+    iFrame. iSplitWith "Hclose2".
+    - iIntros "Hα". iMod ("Hclose2" with "Hα") as "$". done.
+    - iIntros (y) "Hβ". iMod ("Hclose2" with "Hβ") as "$". done.
+  Qed.
+
   (** atomic_update as a fixed-point of the equation
-   AU = ∃ P. ▷ P ∗ □ (▷ P ==∗ α ∗ (α ==∗ AU) ∧ (β ==∗ Q))
-      = ∃ P. ▷ P ∗ □ (▷ P -∗ atomic_acc α AU β Q)
+   AU = make_laterable $ atomic_acc α AU β Q
   *)
-  Context Eo Em α β Φ.
+  Context Eo Ei α β Φ.
 
   Definition atomic_update_pre (Ψ : () → PROP) (_ : ()) : PROP :=
-    (∃ (P : PROP), ▷ P ∗
-     □ (▷ P -∗ atomic_acc Eo (Eo∖Em) α (Ψ ()) β Φ))%I.
+    make_laterable $ atomic_acc Eo Ei α (Ψ ()) β Φ.
 
   Local Instance atomic_update_pre_mono : BiMonoPred atomic_update_pre.
   Proof.
     constructor.
     - iIntros (P1 P2) "#HP12". iIntros ([]) "AU".
-      iDestruct "AU" as (P) "[HP #AS]". iExists P. iFrame.
-      iIntros "!# HP". iApply (atomic_acc_wand with "[HP12]"); last by iApply "AS".
+      iApply (make_laterable_wand with "[] AU").
+      iIntros "!# AA". iApply (atomic_acc_wand with "[HP12] AA").
       iSplit; last by eauto. iApply "HP12".
     - intros ??. solve_proper.
   Qed.
@@ -78,90 +88,229 @@ End definition.
 
 (** Seal it *)
 Definition atomic_update_aux : seal (@atomic_update_def). by eexists. Qed.
-Definition atomic_update `{BiFUpd PROP} {A B : Type} := atomic_update_aux.(unseal) PROP _ A B.
+Definition atomic_update `{BiFUpd PROP} {TA TB : tele} := atomic_update_aux.(unseal) PROP _ TA TB.
 Definition atomic_update_eq :
   @atomic_update = @atomic_update_def := atomic_update_aux.(seal_eq).
 
+Arguments atomic_acc {PROP _ TA TB} Eo Ei _ _ _ _ : simpl never.
+Arguments atomic_update {PROP _ TA TB} Eo Ei _ _ _ : simpl never.
+
+(** Notation: Atomic updates *)
+Notation "'AU' '<<' ∀ x1 .. xn , α '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
+  (atomic_update (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
+                 (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+                 Eo Ei
+                 (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+                       λ x1, .. (λ xn, α%I) ..)
+                 (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+                       λ x1, .. (λ xn,
+                         tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+                         (λ y1, .. (λ yn, β%I) .. )
+                        ) .. )
+                 (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+                       λ x1, .. (λ xn,
+                         tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+                         (λ y1, .. (λ yn, Φ%I) .. )
+                        ) .. )
+  )
+  (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.
+
+Notation "'AU' '<<' ∀ x1 .. xn , α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
+  (atomic_update (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
+                 (TB:=TeleO)
+                 Eo Ei
+                 (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+                       λ x1, .. (λ xn, α%I) ..)
+                 (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+                       λ x1, .. (λ xn, tele_app (TT:=TeleO) β%I) .. )
+                 (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+                       λ 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.
+
+Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
+  (atomic_update (TA:=TeleO)
+                 (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+                 Eo Ei
+                 (tele_app (TT:=TeleO) α%I)
+                 (tele_app (TT:=TeleO) $
+                       tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+                                (λ y1, .. (λ yn, β%I) ..))
+                 (tele_app (TT:=TeleO) $
+                       tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+                                (λ y1, .. (λ yn, Φ%I) ..))
+  )
+  (at level 20, Eo, Ei, α, β, Φ at level 200, y1 binder, yn binder,
+   format "'[   ' 'AU'  '<<'  α  '>>'  '/' @  Eo ,  Ei  '/' '[   ' '<<'  ∃  y1  ..  yn ,  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.
+
+Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
+  (atomic_update (TA:=TeleO) (TB:=TeleO) Eo Ei
+                 (tele_app (TT:=TeleO) α%I)
+                 (tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) β%I)
+                 (tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) Φ%I)
+  )
+  (at level 20, Eo, Ei, α, β, Φ at level 200,
+   format "'[   ' 'AU'  '<<'  α  '>>'  '/' @  Eo ,  Ei  '/' '[   ' '<<'  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.
+
+(** Notation: Atomic accessors *)
+Notation "'AACC' '<<' ∀ x1 .. xn , α 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
+  (atomic_acc (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
+              (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+              Eo Ei
+              (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+                    λ x1, .. (λ xn, α%I) ..)
+              P%I
+              (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+                    λ x1, .. (λ xn,
+                      tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+                      (λ y1, .. (λ yn, β%I) .. )
+                     ) .. )
+              (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+                    λ x1, .. (λ xn,
+                      tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+                      (λ y1, .. (λ yn, Φ%I) .. )
+                     ) .. )
+  )
+  (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.
+
+Notation "'AACC' '<<' ∀ x1 .. xn , α 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
+  (atomic_acc (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
+              (TB:=TeleO)
+              Eo Ei
+              (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+                        λ x1, .. (λ xn, α%I) ..)
+              P%I
+              (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+                        λ x1, .. (λ xn, tele_app (TT:=TeleO) β%I) .. )
+              (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+                        λ 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.
+
+Notation "'AACC' '<<' α 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
+  (atomic_acc (TA:=TeleO)
+              (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+              Eo Ei
+              (tele_app (TT:=TeleO) α%I)
+              P%I
+              (tele_app (TT:=TeleO) $
+                        tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+                        (λ y1, .. (λ yn, β%I) ..))
+              (tele_app (TT:=TeleO) $
+                        tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+                        (λ 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.
+
+Notation "'AACC' '<<' α 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
+  (atomic_acc (TA:=TeleO)
+              (TB:=TeleO)
+              Eo Ei
+              (tele_app (TT:=TeleO) α%I)
+              P%I
+                 (tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) β%I)
+                 (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.
+
 (** Lemmas about AU *)
 Section lemmas.
-  Context `{BiFUpd PROP} {A B : Type}.
-  Implicit Types (α : A → PROP) (β Φ : A → B → PROP) (P : PROP).
+  Context `{BiFUpd PROP} {TA TB : tele}.
+  Implicit Types (α : TA → PROP) (β Φ : TA → TB → PROP) (P : PROP).
 
   Local Existing Instance atomic_update_pre_mono.
 
-  Global Instance atomic_acc_ne Eo Em n :
+  Global Instance atomic_acc_ne Eo Ei n :
     Proper (
-        pointwise_relation A (dist n) ==>
+        pointwise_relation TA (dist n) ==>
         dist n ==>
-        pointwise_relation A (pointwise_relation B (dist n)) ==>
-        pointwise_relation A (pointwise_relation B (dist n)) ==>
+        pointwise_relation TA (pointwise_relation TB (dist n)) ==>
+        pointwise_relation TA (pointwise_relation TB (dist n)) ==>
         dist n
-    ) (atomic_acc (PROP:=PROP) Eo Em).
+    ) (atomic_acc (PROP:=PROP) Eo Ei).
   Proof. solve_proper. Qed.
 
-  Global Instance atomic_update_ne Eo Em n :
+  Global Instance atomic_update_ne Eo Ei n :
     Proper (
-        pointwise_relation A (dist n) ==>
-        pointwise_relation A (pointwise_relation B (dist n)) ==>
-        pointwise_relation A (pointwise_relation B (dist n)) ==>
+        pointwise_relation TA (dist n) ==>
+        pointwise_relation TA (pointwise_relation TB (dist n)) ==>
+        pointwise_relation TA (pointwise_relation TB (dist n)) ==>
         dist n
-    ) (atomic_update (PROP:=PROP) Eo Em).
+    ) (atomic_update (PROP:=PROP) Eo Ei).
   Proof.
     rewrite atomic_update_eq /atomic_update_def /atomic_update_pre. solve_proper.
   Qed.
 
-  (** The ellimination form: an accessor *)
-  Lemma aupd_acc  Eo Em E α β Φ :
-    Eo ⊆ E →
-    atomic_update Eo Em α β Φ -∗
-    atomic_acc E (E∖Em) α (atomic_update Eo Em α β Φ) β Φ.
+  (** The ellimination form: an atomic accessor *)
+  Lemma aupd_aacc  Eo Ei α β Φ :
+    atomic_update Eo Ei α β Φ -∗
+    atomic_acc Eo Ei α (atomic_update Eo Ei α β Φ) β Φ.
   Proof using Type*.
-    rewrite atomic_update_eq {1}/atomic_update_def /=. iIntros (HE) "HUpd".
+    rewrite atomic_update_eq {1}/atomic_update_def /=. iIntros "HUpd".
     iPoseProof (greatest_fixpoint_unfold_1 with "HUpd") as "HUpd".
-    iDestruct "HUpd" as (P) "(HP & Hshift)".
-    iRevert (E HE). iApply atomic_acc_mask.
-    iApply "Hshift". done.
+    iApply make_laterable_elim. done.
   Qed.
 
-  Global Instance aupd_laterable Eo Em α β Φ :
-    Laterable (atomic_update Eo Em α β Φ).
+  (* This lets you eliminate atomic updates with iMod. *)
+  Global Instance elim_mod_aupd φ Eo Ei E α β Φ Q Q' :
+    (∀ R, ElimModal φ false false (|={E,Ei}=> R) R Q Q') →
+    ElimModal (φ ∧ Eo ⊆ E) false false
+              (atomic_update Eo Ei α β Φ)
+              (∃.. x, α x ∗
+                       (α x ={Ei,E}=∗ atomic_update Eo Ei α β Φ) ∧
+                       (∀.. y, β x y ={Ei,E}=∗ Φ x y))
+              Q Q'.
   Proof.
-    rewrite /Laterable atomic_update_eq {1}/atomic_update_def /=. iIntros "AU".
-    iPoseProof (greatest_fixpoint_unfold_1 with "AU") as (P) "[HP #AS]".
-    iExists P. iFrame. iIntros "!# HP !>".
-    iApply greatest_fixpoint_unfold_2. iExists P. iFrame "#∗".
+    intros ?. rewrite /ElimModal /= =>-[??]. iIntros "[AU Hcont]".
+    iPoseProof (aupd_aacc with "AU") as "AC".
+    iMod (atomic_acc_mask_weaken with "AC"); first done.
+    iApply "Hcont". done.
   Qed.
 
-  Lemma aupd_intro P Q α β Eo Em Φ :
+  Global Instance aupd_laterable Eo Ei α β Φ :
+    Laterable (atomic_update Eo Ei α β Φ).
+  Proof.
+    rewrite atomic_update_eq {1}/atomic_update_def greatest_fixpoint_unfold.
+    apply _.
+  Qed.
+
+  Lemma aupd_intro P Q α β Eo Ei Φ :
     Affine P → Persistent P → Laterable Q →
-    (P ∗ Q -∗ atomic_acc Eo (Eo∖Em) α Q β Φ) →
-    P ∗ Q -∗ atomic_update Eo Em α β Φ.
+    (P ∗ Q -∗ atomic_acc Eo Ei α Q β Φ) →
+    P ∗ Q -∗ atomic_update Eo Ei α β Φ.
   Proof.
     rewrite atomic_update_eq {1}/atomic_update_def /=.
     iIntros (??? HAU) "[#HP HQ]".
     iApply (greatest_fixpoint_coind _ (λ _, Q)); last done. iIntros "!#" ([]) "HQ".
-    iDestruct (laterable with "HQ") as (Q') "[HQ' #HQi]". iExists Q'. iFrame.
-    iIntros "!# HQ'". iDestruct ("HQi" with "HQ'") as ">HQ {HQi}".
+    iApply (make_laterable_intro with "[] HQ"). iIntros "!# >HQ".
     iApply HAU. by iFrame.
   Qed.
 
-  Lemma aacc_intro x Eo Ei α P β Φ :
-    Ei ⊆ Eo → α x -∗
-    ((α x ={Eo}=∗ P) ∧ (∀ y, β x y ={Eo}=∗ Φ x y)) -∗
-    atomic_acc Eo Ei α P β Φ.
+  Lemma aacc_intro Eo Ei α P β Φ :
+    Ei ⊆ Eo → (∀.. x, α x -∗
+    ((α x ={Eo}=∗ P) ∧ (∀.. y, β x y ={Eo}=∗ Φ x y)) -∗
+    atomic_acc Eo Ei α P β Φ)%I.
   Proof.
-    iIntros (?) "Hα Hclose".
+    iIntros (? x) "Hα Hclose".
     iMod fupd_intro_mask' as "Hclose'"; last iModIntro; first set_solver.
     iExists x. iFrame. iSplitWith "Hclose".
     - iIntros "Hα". iMod "Hclose'" as "_". iApply "Hclose". done.
     - iIntros (y) "Hβ". iMod "Hclose'" as "_". iApply "Hclose". done.
   Qed.
 
+  (* This lets you open invariants etc. when the goal is an atomic accessor. *)
   Global Instance elim_acc_aacc {X} E1 E2 Ei (α' β' : X → PROP) γ' α β Pas Φ :
     ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1) α' β' γ'
             (atomic_acc E1 Ei α Pas β Φ)
             (λ x', atomic_acc E2 Ei α (β' x' ∗ (γ' x' -∗? Pas))%I β
-                (λ x y, β' x' ∗ (γ' x' -∗? Φ x y)))%I.
+                (λ.. x y, β' x' ∗ (γ' x' -∗? Φ x y))
+            )%I.
   Proof.
     rewrite /ElimAcc.
     (* FIXME: Is there any way to prevent maybe_wand from unfolding?
@@ -176,21 +325,35 @@ Section lemmas.
       iMod ("Hclose" with "Hβ'") as "Hγ'".
       iModIntro. destruct (γ' x'); iApply "HPas"; done.
     - iIntros (y) "Hβ". iMod "Hclose''" as "_".
-      iMod ("Hclose'" with "Hβ") as "[Hβ' HΦ]".
+      iMod ("Hclose'" with "Hβ") as "Hβ'".
+      (* FIXME: Using ssreflect rewrite does not work, see Coq bug #7773. *)
+      rewrite ->!tele_app_bind. iDestruct "Hβ'" as "[Hβ' HΦ]".
       iMod ("Hclose" with "Hβ'") as "Hγ'".
       iModIntro. destruct (γ' x'); iApply "HΦ"; done.
   Qed.
 
-  Lemma aacc_aacc {A' B'} E1 E2 E3
+  (* Everything that fancy updates can eliminate without changing, atomic
+  accessors can eliminate as well.  This is a forwarding instance needed becuase
+  atomic_acc is becoming opaque. *)
+  Global Instance elim_modal_acc p q φ P P' Eo Ei α Pas β Φ :
+    (∀ Q, ElimModal φ p q P P' (|={Eo,Ei}=> Q) (|={Eo,Ei}=> Q)) →
+    ElimModal φ p q P P'
+              (atomic_acc Eo Ei α Pas β Φ)
+              (atomic_acc Eo Ei α Pas β Φ).
+  Proof. intros Helim. apply Helim. Qed.
+
+  Lemma aacc_aacc {TA' TB' : tele} E1 E1' E2 E3
         α P β Φ
-        (α' : A' → PROP) P' (β' Φ' : A' → B' → PROP) :
-    atomic_acc E1 E2 α P β Φ -∗
-    (∀ x, α x -∗ atomic_acc E2 E3 α' (α x ∗ (P ={E1}=∗ P')) β'
-            (λ x' y', (α x ∗ (P ={E1}=∗ Φ' x' y'))
-                    ∨ ∃ y, β x y ∗ (Φ x y ={E1}=∗ Φ' x' y'))) -∗
+        (α' : TA' → PROP) P' (β' Φ' : TA' → TB' → PROP) :
+    E1' ⊆ E1 →
+    atomic_acc E1' E2 α P β Φ -∗
+    (∀.. x, α x -∗ atomic_acc E2 E3 α' (α x ∗ (P ={E1}=∗ P')) β'
+            (λ.. x' y', (α x ∗ (P ={E1}=∗ Φ' x' y'))
+                    ∨ ∃.. y, β x y ∗ (Φ x y ={E1}=∗ Φ' x' y'))) -∗
     atomic_acc E1 E3 α' P' β' Φ'.
   Proof.
-    iIntros "Hupd Hstep". iMod ("Hupd") as (x) "[Hα Hclose]".
+    iIntros (?) "Hupd Hstep".
+    iMod (atomic_acc_mask_weaken with "Hupd") as (x) "[Hα Hclose]"; first done.
     iMod ("Hstep" with "Hα") as (x') "[Hα' Hclose']".
     iModIntro. iExists x'. iFrame "Hα'". iSplit.
     - iIntros "Hα'". iDestruct "Hclose'" as "[Hclose' _]".
@@ -198,7 +361,9 @@ Section lemmas.
       iDestruct "Hclose" as "[Hclose _]".
       iMod ("Hclose" with "Hα"). iApply "Hupd". auto.
     - iIntros (y') "Hβ'". iDestruct "Hclose'" as "[_ Hclose']".
-      iMod ("Hclose'" with "Hβ'") as "[[Hα HΦ']|Hcont]".
+      iMod ("Hclose'" with "Hβ'") as "Hres".
+      (* FIXME: Using ssreflect rewrite does not work, see Coq bug #7773. *)
+      rewrite ->!tele_app_bind. iDestruct "Hres" as "[[Hα HΦ']|Hcont]".
       + (* Abort the step we are eliminating *)
         iDestruct "Hclose" as "[Hclose _]".
         iMod ("Hclose" with "Hα") as "HP".
@@ -210,64 +375,65 @@ Section lemmas.
         iApply "HΦ'". done.
   Qed.
 
-  Lemma aacc_aupd {A' B'} E1 E2 Eo Em
+  Lemma aacc_aupd {TA' TB' : tele} E1 E1' E2 E3
         α β Φ
-        (α' : A' → PROP) P' (β' Φ' : A' → B' → PROP) :
-    Eo ⊆ E1 →
-    atomic_update Eo Em α β Φ -∗
-    (∀ x, α x -∗ atomic_acc (E1∖Em) E2 α' (α x ∗ (atomic_update Eo Em α β Φ ={E1}=∗ P')) β'
-            (λ x' y', (α x ∗ (atomic_update Eo Em α β Φ ={E1}=∗ Φ' x' y'))
-                    ∨ ∃ y, β x y ∗ (Φ x y ={E1}=∗ Φ' x' y'))) -∗
-    atomic_acc E1 E2 α' P' β' Φ'.
+        (α' : TA' → PROP) P' (β' Φ' : TA' → TB' → PROP) :
+    E1' ⊆ E1 →
+    atomic_update E1' E2 α β Φ -∗
+    (∀.. x, α x -∗ atomic_acc E2 E3 α' (α x ∗ (atomic_update E1' E2 α β Φ ={E1}=∗ P')) β'
+            (λ.. x' y', (α x ∗ (atomic_update E1' E2 α β Φ ={E1}=∗ Φ' x' y'))
+                    ∨ ∃.. y, β x y ∗ (Φ x y ={E1}=∗ Φ' x' y'))) -∗
+    atomic_acc E1 E3 α' P' β' Φ'.
   Proof.
-    iIntros (?) "Hupd Hstep". iApply (aacc_aacc with "[Hupd] Hstep").
-    iApply aupd_acc; done.
+    iIntros (?) "Hupd Hstep". iApply (aacc_aacc with "[Hupd] Hstep"); first done.
+    iApply aupd_aacc; done.
   Qed.
 
-  Lemma aacc_aupd_commit {A' B'} E1 E2 Eo Em
+  Lemma aacc_aupd_commit {TA' TB' : tele} E1 E1' E2 E3
         α β Φ
-        (α' : A' → PROP) P' (β' Φ' : A' → B' → PROP) :
-    Eo ⊆ E1 →
-    atomic_update Eo Em α β Φ -∗
-    (∀ x, α x -∗ atomic_acc (E1∖Em) E2 α' (α x ∗ (atomic_update Eo Em α β Φ ={E1}=∗ P')) β'
-            (λ x' y', ∃ y, β x y ∗ (Φ x y ={E1}=∗ Φ' x' y'))) -∗
-    atomic_acc E1 E2 α' P' β' Φ'.
+        (α' : TA' → PROP) P' (β' Φ' : TA' → TB' → PROP) :
+    E1' ⊆ E1 →
+    atomic_update E1' E2 α β Φ -∗
+    (∀.. x, α x -∗ atomic_acc E2 E3 α' (α x ∗ (atomic_update E1' E2 α β Φ ={E1}=∗ P')) β'
+            (λ.. x' y', ∃.. y, β x y ∗ (Φ x y ={E1}=∗ Φ' x' y'))) -∗
+    atomic_acc E1 E3 α' P' β' Φ'.
   Proof.
     iIntros (?) "Hupd Hstep". iApply (aacc_aupd with "Hupd"); first done.
     iIntros (x) "Hα". iApply atomic_acc_wand; last first.
     { iApply "Hstep". done. }
-    iSplit; first by eauto. iIntros (??) "?". by iRight.
+    (* FIXME: Using ssreflect rewrite does not work, see Coq bug #7773. *)
+    iSplit; first by eauto. iIntros (??) "?". rewrite ->!tele_app_bind. by iRight.
   Qed.
 
-  Lemma aacc_aupd_abort {A' B'} E1 E2 Eo Em
+  Lemma aacc_aupd_abort {TA' TB' : tele} E1 E1' E2 E3
         α β Φ
-        (α' : A' → PROP) P' (β' Φ' : A' → B' → PROP) :
-    Eo ⊆ E1 →
-    atomic_update Eo Em α β Φ -∗
-    (∀ x, α x -∗ atomic_acc (E1∖Em) E2 α' (α x ∗ (atomic_update Eo Em α β Φ ={E1}=∗ P')) β'
-            (λ x' y', α x ∗ (atomic_update Eo Em α β Φ ={E1}=∗ Φ' x' y'))) -∗
-    atomic_acc E1 E2 α' P' β' Φ'.
+        (α' : TA' → PROP) P' (β' Φ' : TA' → TB' → PROP) :
+    E1' ⊆ E1 →
+    atomic_update E1' E2 α β Φ -∗
+    (∀.. x, α x -∗ atomic_acc E2 E3 α' (α x ∗ (atomic_update E1' E2 α β Φ ={E1}=∗ P')) β'
+            (λ.. x' y', α x ∗ (atomic_update E1' E2 α β Φ ={E1}=∗ Φ' x' y'))) -∗
+    atomic_acc E1 E3 α' P' β' Φ'.
   Proof.
     iIntros (?) "Hupd Hstep". iApply (aacc_aupd with "Hupd"); first done.
     iIntros (x) "Hα". iApply atomic_acc_wand; last first.
     { iApply "Hstep". done. }
-    iSplit; first by eauto. iIntros (??) "?". by iLeft.
+    (* FIXME: Using ssreflect rewrite does not work, see Coq bug #7773. *)
+    iSplit; first by eauto. iIntros (??) "?". rewrite ->!tele_app_bind. by iLeft.
   Qed.
 
 End lemmas.
 
 (** ProofMode support for atomic updates *)
-
 Section proof_mode.
-  Context `{BiFUpd PROP} {A B : Type}.
-  Implicit Types (α : A → PROP) (β Φ : A → B → PROP) (P : PROP).
+  Context `{BiFUpd PROP} {TA TB : tele}.
+  Implicit Types (α : TA → PROP) (β Φ : TA → TB → PROP) (P : PROP).
 
-  Lemma tac_aupd_intro Γp Γs n α β Eo Em Φ P :
+  Lemma tac_aupd_intro Γp Γs n α β Eo Ei Φ P :
     Timeless (PROP:=PROP) emp →
     TCForall Laterable (env_to_list Γs) →
     P = prop_of_env Γs →
-    envs_entails (Envs Γp Γs n) (atomic_acc Eo (Eo∖Em) α P β Φ) →
-    envs_entails (Envs Γp Γs n) (atomic_update Eo Em α β Φ).
+    envs_entails (Envs Γp Γs n) (atomic_acc Eo Ei α P β Φ) →
+    envs_entails (Envs Γp Γs n) (atomic_update Eo Ei α β Φ).
   Proof.
     intros ? HΓs ->. rewrite envs_entails_eq of_envs_eq' /atomic_acc /=.
     setoid_rewrite prop_of_env_sound =>HAU.
@@ -283,3 +449,13 @@ Tactic Notation "iAuIntro" :=
   | iSolveTC || fail "iAuIntro: not all spatial assumptions are laterable"
   | (* P = ...: make the P pretty *) pm_reflexivity
   | (* the new proof mode goal *) ].
+Tactic Notation "iAaccIntro" "with" constr(sel) :=
+  iStartProof; lazymatch goal with
+  | |- environments.envs_entails _ (@atomic_acc ?PROP ?H ?TA ?TB ?Eo ?Ei ?α ?P ?β ?Φ) =>
+    iApply (@aacc_intro PROP H TA TB Eo Ei α P β Φ with sel);
+    first try solve_ndisj; last iSplit
+  | _ => fail "iAAccIntro: Goal is not an atomic accessor"
+  end.
+
+(* From here on, prevent TC search from implicitly unfolding these. *)
+Typeclasses Opaque atomic_acc atomic_update.
diff --git a/theories/bi/lib/laterable.v b/theories/bi/lib/laterable.v
index a1243539d128962bf206b27414e0d344628c93c4..155df72d47662abedd09a87cd84e585ab4f2aff8 100644
--- a/theories/bi/lib/laterable.v
+++ b/theories/bi/lib/laterable.v
@@ -14,6 +14,9 @@ Section instances.
   Implicit Types P : PROP.
   Implicit Types Ps : list PROP.
 
+  Global Instance laterable_proper : Proper ((⊣⊢) ==> (↔)) (@Laterable PROP).
+  Proof. solve_proper. Qed.
+
   Global Instance later_laterable P : Laterable (â–· P).
   Proof.
     rewrite /Laterable. iIntros "HP". iExists P. iFrame.
@@ -57,4 +60,44 @@ Section instances.
     TCForall Laterable Ps →
     Laterable ([∗] Ps).
   Proof. induction 2; simpl; apply _. Qed.
+
+  (* A wrapper to obtain a weaker, laterable form of any assertion. *)
+  Definition make_laterable (Q : PROP) : PROP :=
+    (∃ P, ▷ P ∗ □ (▷ P -∗ Q))%I.
+
+  Global Instance make_laterable_ne : NonExpansive make_laterable.
+  Proof. solve_proper. Qed.
+  Global Instance make_laterable_proper : Proper ((≡) ==> (≡)) make_laterable := ne_proper _.
+
+  Lemma make_laterable_wand Q1 Q2 :
+    □ (Q1 -∗ Q2) -∗ (make_laterable Q1 -∗ make_laterable Q2).
+  Proof.
+    iIntros "#HQ HQ1". iDestruct "HQ1" as (P) "[HP #HQ1]".
+    iExists P. iFrame. iIntros "!# HP". iApply "HQ". iApply "HQ1". done.
+  Qed.
+
+  Global Instance make_laterable_laterable Q :
+    Laterable (make_laterable Q).
+  Proof.
+    rewrite /Laterable. iIntros "HQ". iDestruct "HQ" as (P) "[HP #HQ]".
+    iExists P. iFrame. iIntros "!# HP !>". iExists P. by iFrame.
+  Qed.
+
+  Lemma make_laterable_elim Q :
+    make_laterable Q -∗ Q.
+  Proof.
+    iIntros "HQ". iDestruct "HQ" as (P) "[HP #HQ]". by iApply "HQ".
+  Qed.
+
+  Lemma make_laterable_intro P Q :
+    Laterable P →
+    □ (◇ P -∗ Q) -∗ P -∗ make_laterable Q.
+  Proof.
+    iIntros (?) "#HQ HP".
+    iDestruct (laterable with "HP") as (P') "[HP' #HPi]". iExists P'.
+    iFrame. iIntros "!# HP'". iApply "HQ". iApply "HPi". done.
+  Qed.
+
 End instances.
+
+Typeclasses Opaque make_laterable.
diff --git a/theories/heap_lang/lib/atomic_heap.v b/theories/heap_lang/lib/atomic_heap.v
index ad3f079a38ab3281c597ca7b9ed075d1ccbbcd12..a11b7c1620c34c9d5be813e8e59fa1aa236b5433 100644
--- a/theories/heap_lang/lib/atomic_heap.v
+++ b/theories/heap_lang/lib/atomic_heap.v
@@ -1,52 +1,64 @@
 From iris.heap_lang Require Export lifting notation.
-From iris.base_logic.lib Require Export invariants.
 From iris.program_logic Require Export atomic.
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
+From iris.bi.lib Require Import fractional.
 Set Default Proof Using "Type".
 
 (** A general logically atomic interface for a heap. *)
-Structure atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
+Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
   (* -- operations -- *)
   alloc : val;
   load : val;
   store : val;
   cas : val;
   (* -- predicates -- *)
-  (* name is used to associate locked with is_lock *)
   mapsto (l : loc) (q: Qp) (v : val) : iProp Σ;
-  (* -- general properties -- *)
-  mapsto_timeless l q v : Timeless (mapsto l q v);
+  (* -- mapsto properties -- *)
+  mapsto_timeless l q v :> Timeless (mapsto l q v);
+  mapsto_fractional l v :> Fractional (λ q, mapsto l q v);
+  mapsto_as_fractional l q v :>
+    AsFractional (mapsto l q v) (λ q, mapsto l q v) q;
+  mapsto_agree l q1 q2 v1 v2 :> mapsto l q1 v1 -∗ mapsto l q2 v2 -∗ ⌜v1 = v2⌝;
   (* -- operation specs -- *)
-  alloc_spec v :
-    {{{ True }}} alloc v {{{ l, RET #l; mapsto l 1 v }}};
+  alloc_spec e v :
+    IntoVal e v → {{{ True }}} alloc e {{{ l, RET #l; mapsto l 1 v }}};
   load_spec (l : loc) :
-    atomic_wp (load #l)%E
-              ⊤ ⊤
-              (λ '(v, q), mapsto l q v)
-              (λ '(v, q) (_:()), mapsto l q v)
-              (λ '(v, q) _, v);
+    <<< ∀ (v : val) q, mapsto l q v >>> load #l @ ⊤ <<< mapsto l q v, RET v >>>;
   store_spec (l : loc) (e : expr) (w : val) :
     IntoVal e w →
-    atomic_wp (store (#l, e))%E
-              ⊤ ⊤
-              (λ v, mapsto l 1 v)
-              (λ v (_:()), mapsto l 1 w)
-              (λ _ _, #()%V);
+    <<< ∀ v, mapsto l 1 v >>> store (#l, e) @ ⊤
+    <<< mapsto l 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]
   is outside the atomic triple, which makes it much easier to use -- and the
   spec is still good enough for all our applications. *)
   cas_spec (l : loc) (e1 e2 : expr) (w1 w2 : val) :
     IntoVal e1 w1 → IntoVal e2 w2 → val_is_unboxed w1 →
-    atomic_wp (cas (#l, e1, e2))%E
-              ⊤ ⊤
-              (λ v, mapsto l 1 v)%I
-              (λ v (_:()), if decide (v = w1) then mapsto l 1 w2 else mapsto l 1 v)
-              (λ v _, #(if decide (v = w1) then true else false)%V);
+    <<< ∀ v, mapsto l 1 v >>> cas (#l, e1, e2) @ ⊤
+    <<< if decide (v = w1) then mapsto l 1 w2 else mapsto l 1 v,
+        RET #(if decide (v = w1) then true else false) >>>;
 }.
 Arguments atomic_heap _ {_}.
 
+(** Notation for heap primitives, in a module so you can import it separately. *)
+Module notation.
+Notation "l ↦{ q } v" := (mapsto l q v)
+  (at level 20, q at level 50, format "l  ↦{ q }  v") : bi_scope.
+Notation "l ↦ v" := (mapsto l 1 v) (at level 20) : bi_scope.
+
+Notation "l ↦{ q } -" := (∃ v, l ↦{q} v)%I
+  (at level 20, q at level 50, format "l  ↦{ q }  -") : bi_scope.
+Notation "l ↦ -" := (l ↦{1} -)%I (at level 20) : bi_scope.
+
+Notation "'ref' e" := (alloc e) : expr_scope.
+Notation "! e" := (load e) : expr_scope.
+Notation "e1 <- e2" := (store (e1, e2)%E) : expr_scope.
+
+Notation CAS e1 e2 e3 := (cas (e1, e2, e3)%E).
+
+End notation.
+
 (** Proof that the primitive physical operations of heap_lang satisfy said interface. *)
 Definition primitive_alloc : val :=
   λ: "v", ref "v".
@@ -60,54 +72,50 @@ Definition primitive_cas : val :=
 Section proof.
   Context `{!heapG Σ}.
 
-  Lemma primitive_alloc_spec v :
-    {{{ True }}} primitive_alloc v {{{ l, RET #l; l ↦ v }}}.
+  Lemma primitive_alloc_spec e v :
+    IntoVal e v → {{{ True }}} primitive_alloc e {{{ l, RET #l; l ↦ v }}}.
   Proof.
-    iIntros (Φ) "_ HΦ". wp_let. wp_alloc l. iApply "HΦ". done.
+    iIntros (<- Φ) "_ HΦ". wp_let. wp_alloc l. iApply "HΦ". done.
   Qed.
 
   Lemma primitive_load_spec (l : loc) :
-    atomic_wp (primitive_load #l)%E
-              ⊤ ⊤
-              (λ '(v, q), l ↦{q} v)%I
-              (λ '(v, q) (_:()), l ↦{q} v)%I
-              (λ '(v, q) _, v).
+    <<< ∀ (v : val) q, l ↦{q} v >>> primitive_load #l @ ⊤
+    <<< l ↦{q} v, RET v >>>.
   Proof.
     iIntros (Q Φ) "? AU". wp_let.
-    iMod (aupd_acc with "AU") as ((v, q)) "[H↦ [_ Hclose]]"; first solve_ndisj.
-    wp_load. iMod ("Hclose" $! () with "H↦") as "HΦ". by iApply "HΦ".
+    iMod "AU" as (v q) "[H↦ [_ Hclose]]".
+    wp_load. iMod ("Hclose" with "H↦") as "HΦ". by iApply "HΦ".
   Qed.
 
   Lemma primitive_store_spec (l : loc) (e : expr) (w : val) :
     IntoVal e w →
-    atomic_wp (primitive_store (#l, e))%E
-              ⊤ ⊤
-              (λ v, l ↦ v)%I
-              (λ v (_:()), l ↦ w)%I
-              (λ _ _, #()%V).
+    <<< ∀ v, l ↦ v >>> primitive_store (#l, e) @ ⊤
+    <<< l ↦ w, RET #() >>>.
   Proof.
     iIntros (<- Q Φ) "? AU". wp_let. wp_proj. wp_proj.
-    iMod (aupd_acc with "AU") as (v) "[H↦ [_ Hclose]]"; first solve_ndisj.
-    wp_store. iMod ("Hclose" $! () with "H↦") as "HΦ". by iApply "HΦ".
+    iMod "AU" as (v) "[H↦ [_ Hclose]]".
+    wp_store. iMod ("Hclose" with "H↦") as "HΦ". by iApply "HΦ".
   Qed.
 
   Lemma primitive_cas_spec (l : loc) e1 e2 (w1 w2 : val) :
     IntoVal e1 w1 → IntoVal e2 w2 → val_is_unboxed w1 →
-    atomic_wp (primitive_cas (#l, e1, e2))%E
-              ⊤ ⊤
-              (λ v, l ↦ v)%I
-              (λ v (_:()), if decide (v = w1) then l ↦ w2 else l ↦ v)%I
-              (λ v _, #(if decide (v = w1) then true else false)%V).
+    <<< ∀ (v : val), l ↦ v >>>
+      primitive_cas (#l, e1, e2) @ ⊤
+    <<< if decide (v = w1) then l ↦ w2 else l ↦ v,
+        RET #(if decide (v = w1) then true else false) >>>.
   Proof.
     iIntros (<- <- ? Q Φ) "? AU". wp_let. repeat wp_proj.
-    iMod (aupd_acc with "AU") as (v) "[H↦ [_ Hclose]]"; first solve_ndisj.
+    iMod "AU" as (v) "[H↦ [_ Hclose]]".
     destruct (decide (v = w1)) as [<-|Hv]; [wp_cas_suc|wp_cas_fail];
-    iMod ("Hclose" $! () with "H↦") as "HΦ"; by iApply "HΦ".
+    iMod ("Hclose" with "H↦") as "HΦ"; by iApply "HΦ".
   Qed.
-
-  Definition primitive_atomic_heap : atomic_heap Σ :=
-    {| alloc_spec := primitive_alloc_spec;
-       load_spec := primitive_load_spec;
-       store_spec := primitive_store_spec;
-       cas_spec := primitive_cas_spec |}.
 End proof.
+
+(* NOT an instance because users should choose explicitly to use it
+     (using [Explicit Instance]). *)
+Definition primitive_atomic_heap `{!heapG Σ} : atomic_heap Σ :=
+  {| alloc_spec := primitive_alloc_spec;
+     load_spec := primitive_load_spec;
+     store_spec := primitive_store_spec;
+     cas_spec := primitive_cas_spec;
+     mapsto_agree := gen_heap.mapsto_agree  |}.
diff --git a/theories/heap_lang/lib/increment.v b/theories/heap_lang/lib/increment.v
index 4640f7c0167214e2bc091b1c408e6280dae655ae..d26b432921e628ef895f04b0e8e2ae8fcea62bdb 100644
--- a/theories/heap_lang/lib/increment.v
+++ b/theories/heap_lang/lib/increment.v
@@ -2,51 +2,73 @@ From iris.base_logic.lib Require Export invariants.
 From iris.program_logic Require Export atomic.
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation atomic_heap par.
+From iris.bi.lib Require Import fractional.
 Set Default Proof Using "Type".
 
 (** Show that implementing fetch-and-add on top of CAS preserves logical
 atomicity. *)
 
-(* TODO: Move this to iris-examples once gen_proofmode is merged. *)
 Section increment.
-  Context `{!heapG Σ} (aheap: atomic_heap Σ).
+  Context `{!heapG Σ} {aheap: atomic_heap Σ}.
+
+  Import atomic_heap.notation.
 
   Definition incr: val :=
     rec: "incr" "l" :=
-       let: "oldv" := aheap.(load) "l" in
-       if: aheap.(cas) ("l", "oldv", ("oldv" + #1))
+       let: "oldv" := !"l" in
+       if: CAS "l" "oldv" ("oldv" + #1)
          then "oldv" (* return old value if success *)
          else "incr" "l".
 
   Lemma incr_spec (l: loc) :
-        atomic_wp (incr #l)
-                  ⊤ ⊤
-                  (λ (v: Z), aheap.(mapsto) l 1 #v)%I
-                  (λ v (_:()), aheap.(mapsto) l 1 #(v + 1))%I
-                  (λ v _, #v).
+    <<< ∀ (v : Z), l ↦ #v >>> incr #l @ ⊤ <<< l ↦ #(v + 1), RET #v >>>.
   Proof.
-    iIntros (Q Φ) "HQ AU". iLöb as "IH". wp_let.
-    wp_apply (load_spec with "[HQ]"); first by iAccu.
-    (* Prove the atomic shift for load *)
+    iApply wp_atomic_intro. iIntros (Φ) "AU". iLöb as "IH". wp_let.
+    wp_apply load_spec; first by iAccu.
+    (* Prove the atomic update for load *)
     iAuIntro. iApply (aacc_aupd_abort with "AU"); first done.
-    iIntros (x) "H↦".
-    iApply (aacc_intro (_, _) with "[H↦]"); [solve_ndisj|done|iSplit].
-    { iIntros "$ !> $ !> //". }
-    iIntros ([]) "$ !> AU !> HQ".
+    iIntros (x) "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
+    iIntros "$ !> AU !> _".
     (* Now go on *)
-    wp_let. wp_op. wp_bind (aheap.(cas) _)%I.
-    wp_apply (cas_spec with "[HQ]"); first done; first by iAccu.
-    (* Prove the atomic shift for CAS *)
+    wp_let. wp_op. wp_bind (CAS _ _ _)%I.
+    wp_apply cas_spec; [done|iAccu|].
+    (* Prove the atomic update for CAS *)
     iAuIntro. iApply (aacc_aupd with "AU"); first done.
-    iIntros (x') "H↦".
-    iApply (aacc_intro with "[H↦]"); [solve_ndisj|done|iSplit].
-    { eauto 10 with iFrame. }
-    iIntros ([]) "H↦ !>".
+    iIntros (x') "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
+    iIntros "H↦ !>".
     destruct (decide (#x' = #x)) as [[= ->]|Hx].
-    - iRight. iExists (). iFrame. iIntros "HΦ !> HQ".
+    - iRight. iFrame. iIntros "HΦ !> _".
       wp_if. by iApply "HΦ".
-    - iLeft. iFrame. iIntros "AU !> HQ".
-      wp_if. iApply ("IH" with "HQ"). done.
+    - iLeft. iFrame. iIntros "AU !> _".
+      wp_if. iApply "IH". done.
+  Qed.
+
+  Definition weak_incr: val :=
+    rec: "weak_incr" "l" :=
+       let: "oldv" := !"l" in
+       "l" <- ("oldv" + #1);;
+       "oldv" (* return old value *).
+
+  (* TODO: Generalize to q and 1-q, based on some theory for a "maybe-mapsto"
+     connective that works on [option Qp] (the type of 1-q). *)
+  Lemma weak_incr_spec (l: loc) (v : Z) :
+    l ↦{1/2} #v -∗
+    <<< ∀ (v' : Z), l ↦{1/2} #v' >>>
+      weak_incr #l @ ⊤
+    <<< ⌜v = v'⌝ ∗ l ↦ #(v + 1), RET #v >>>.
+  Proof.
+    iIntros "Hl". iApply wp_atomic_intro. iIntros (Φ) "AU". wp_let.
+    wp_apply (atomic_wp_seq $! (load_spec _) with "Hl").
+    iIntros "Hl". wp_let. wp_op.
+    wp_apply store_spec; first by iAccu.
+    (* Prove the atomic update for store *)
+    iAuIntro. iApply (aacc_aupd_commit with "AU"); first done.
+    iIntros (x) "H↦".
+    iDestruct (mapsto_agree with "Hl H↦") as %[= <-].
+    iCombine "Hl" "H↦" as "Hl". iAaccIntro with "Hl".
+    { iIntros "[$ $]"; eauto. }
+    iIntros "$ !>". iSplit; first done.
+    iIntros "HΦ !> _". wp_seq. done.
   Qed.
 
 End increment.
@@ -54,10 +76,12 @@ End increment.
 Section increment_client.
   Context `{!heapG Σ, !spawnG Σ}.
 
+  Existing Instance primitive_atomic_heap.
+
   Definition incr_client : val :=
     λ: "x",
        let: "l" := ref "x" in
-       incr primitive_atomic_heap "l" ||| incr primitive_atomic_heap "l".
+       incr "l" ||| incr "l".
 
   Lemma incr_client_safe (x: Z):
     WP incr_client #x {{ _, True }}%I.
@@ -66,12 +90,10 @@ Section increment_client.
     iMod (inv_alloc nroot _ (∃x':Z, l ↦ #x')%I with "[Hl]") as "#Hinv"; first eauto.
     (* FIXME: I am only using persistent stuff, so I should be allowed
        to move this to the persisten context even without the additional â–¡. *)
-    iAssert (â–¡ WP incr primitive_atomic_heap #l {{ _, True }})%I as "#Aupd".
-    { iAlways. wp_apply (incr_spec with "[]"); first by iAccu. clear x.
-      iAuIntro. iInv nroot as (x) ">H↦".
-      iApply (aacc_intro with "[H↦]"); [solve_ndisj|done|iSplit].
-      { by eauto 10. }
-      iIntros ([]) "H↦ !>". iSplitL "H↦"; first by eauto 10.
+    iAssert (â–¡ WP incr #l {{ _, True }})%I as "#Aupd".
+    { iAlways. wp_apply incr_spec; first by iAccu. clear x.
+      iAuIntro. iInv nroot as (x) ">H↦". iAaccIntro with "H↦"; first by eauto 10.
+      iIntros "H↦ !>". iSplitL "H↦"; first by eauto 10.
       (* The continuation: From after the atomic triple to the postcondition of the WP *)
       done.
     }
diff --git a/theories/program_logic/atomic.v b/theories/program_logic/atomic.v
index b8a395fc27f0fec783b494f375b851fae292c7d5..9c0df10983a554c10c2b9b16c4c756827cdbca3d 100644
--- a/theories/program_logic/atomic.v
+++ b/theories/program_logic/atomic.v
@@ -1,16 +1,138 @@
+From stdpp Require Import namespaces.
 From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import tactics classes.
 From iris.bi.lib Require Export atomic.
+From iris.bi Require Import telescopes.
 Set Default Proof Using "Type".
 
-Definition atomic_wp `{irisG Λ Σ} {A B : Type}
+(* This hard-codes the inner mask to be empty, because we have yet to find an
+example where we want it to be anything else. *)
+Definition atomic_wp `{irisG Λ Σ} {TA TB : tele}
   (e: expr Λ) (* expression *)
-  (Eo Em : coPset) (* outside/module masks *)
-  (α: A → iProp Σ) (* atomic pre-condition *)
-  (β: A → B → iProp Σ) (* atomic post-condition *)
-  (f: A → B → val Λ) (* Turn the return data into the return value *)
+  (Eo : coPset) (* (outer) 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 Σ :=
-    (∀ Q Φ, Q -∗ atomic_update Eo Em α β (λ x y, Q -∗ Φ (f x y)) -∗
+    (∀ Q (Φ : val Λ → iProp Σ), Q -∗
+             atomic_update Eo ∅ α β (λ.. x y, Q -∗ Φ (f x y)) -∗
              WP e {{ Φ }})%I.
 (* Note: To add a private postcondition, use
-   atomic_update α β Eo Em (λ x y, POST x y -∗ Φ (f x y)) *)
+   atomic_update α β Eo Ei (λ x y, POST x y -∗ Φ (f x y)) *)
+
+Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ Eo '<<<' ∃ y1 .. yn , β , 'RET' v '>>>'" :=
+  (atomic_wp (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
+             (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+             e%E
+             Eo
+             (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+                       λ x1, .. (λ xn, α%I) ..)
+             (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+                       λ x1, .. (λ xn,
+                         tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+                         (λ y1, .. (λ yn, β%I) .. )
+                        ) .. )
+             (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+                       λ x1, .. (λ xn,
+                         tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+                         (λ 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  '>>>' ']' ']'")
+  : stdpp_scope.
+
+Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ Eo '<<<' β , 'RET' v '>>>'" :=
+  (atomic_wp (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
+             (TB:=TeleO)
+             e%E
+             Eo
+             (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+                       λ x1, .. (λ xn, α%I) ..)
+             (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+                       λ x1, .. (λ xn,
+                         tele_app (TT:=TeleO) β%I
+                        ) .. )
+             (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+                       λ x1, .. (λ xn,
+                         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  '>>>' ']' ']'")
+  : stdpp_scope.
+
+Notation "'<<<' α '>>>' e @ Eo '<<<' ∃ y1 .. yn , β , 'RET' v '>>>'" :=
+  (atomic_wp (TA:=TeleO)
+             (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+             e%E
+             Eo
+             (tele_app (TT:=TeleO) α%I)
+             (tele_app (TT:=TeleO) $
+                       tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+                         (λ y1, .. (λ yn, β%I) .. ))
+             (tele_app (TT:=TeleO) $
+                       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  '>>>' ']' ']'")
+  : stdpp_scope.
+
+Notation "'<<<' α '>>>' e @ Eo '<<<' β , 'RET' v '>>>'" :=
+  (atomic_wp (TA:=TeleO)
+             (TB:=TeleO)
+             e%E
+             Eo
+             (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  '>>>' ']' ']'")
+  : stdpp_scope.
+
+(** Theory *)
+Section lemmas.
+  Context `{irisG Λ Σ} {TA TB : tele}.
+  Notation iProp := (iProp Σ).
+  Implicit Types (α : TA → iProp) (β : TA → TB → iProp) (f : TA → TB → val Λ).
+
+  Lemma atomic_wp_seq e Eo α β f {HL : ∀.. x, Laterable (α x)} :
+    atomic_wp e Eo α β f -∗
+    ∀ Φ, ∀.. x, α x -∗ (∀.. y, β x y -∗ Φ (f x y)) -∗ WP e {{ Φ }}.
+  Proof.
+    rewrite ->tforall_forall in HL.
+    iIntros "Hwp" (Φ x) "Hα HΦ". iApply ("Hwp" with "[HΦ]"); first iAccu.
+    iAuIntro. iAaccIntro with "Hα"; first by eauto. iIntros (y) "Hβ !>".
+    (* FIXME: Using ssreflect rewrite does not work, see Coq bug #7773. *)
+    rewrite ->!tele_app_bind. iIntros "HΦ". iApply "HΦ". done.
+  Qed.
+
+  (* Sequential triples with a persistent precondition and no initial quantifier
+  are atomic. *)
+  Lemma seq_wp_atomic e Eo (α : [tele] → iProp) (β : [tele] → TB → iProp)
+        (f : [tele] → TB → val Λ) {HP : ∀.. x, Persistent (α x)} :
+    (∀ Φ, ∀.. x, α x -∗ (∀.. y, β x y -∗ Φ (f x y)) -∗ WP e {{ Φ }}) -∗
+    atomic_wp e Eo α β f.
+  Proof.
+    simpl in HP. iIntros "Hwp" (Q Φ) "HQ HΦ". iApply fupd_wp.
+    iMod ("HΦ") as "[#Hα [Hclose _]]". iMod ("Hclose" with "Hα") as "HΦ".
+    iApply wp_fupd. iApply ("Hwp" with "Hα"). iIntros "!>" (y) "Hβ".
+    iMod ("HΦ") as "[_ [_ Hclose]]". iMod ("Hclose" with "Hβ") as "HΦ".
+    (* FIXME: Using ssreflect rewrite does not work, see Coq bug #7773. *)
+    rewrite ->!tele_app_bind. iApply "HΦ". done.
+  Qed.
+
+  (* Way to prove an atomic triple without seeing the Q *)
+  Lemma wp_atomic_intro e Eo α β f :
+    (∀ (Φ : val Λ → iProp),
+             atomic_update Eo ∅ α β (λ.. x y, Φ (f x y)) -∗
+             WP e {{ Φ }}) -∗
+    atomic_wp e Eo α β f.
+  Proof.
+    iIntros "Hwp" (Q Φ) "HQ AU". iApply (wp_wand with "[-HQ]").
+    { iApply ("Hwp" $! (λ v, Q -∗ Φ v)%I). done. }
+    iIntros (v) "HΦ". iApply "HΦ". done.
+  Qed.
+End lemmas.