diff --git a/tests/atomic.8.8.ref b/tests/atomic.8.8.ref
index 238708315a1656731ecc3a853489338db7c99e9d..a3f9185273b897d0d0eebbbde3e4ec0a5bd52004 100644
--- a/tests/atomic.8.8.ref
+++ b/tests/atomic.8.8.ref
@@ -1,3 +1,17 @@
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  aheap : atomic_heap Σ
+  Q : iProp Σ
+  l : loc
+  v : val
+  ============================
+  "Hl" : l ↦ v
+  --------------------------------------∗
+  AACC << ∀ (v0 : val) (q : Qp), l ↦{q} v0 ABORT l ↦ v >> @ ⊤, ∅
+       << l ↦{q} v0, COMM Q -∗ Q >>
+  
 1 subgoal
   
   Σ : gFunctors
@@ -10,11 +24,9 @@
   Σ : 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 -∗ Φ #() >>
+  "AU" : AU << ∀ x : val, P x >> @ ⊤, ∅ << ∃ y : val, P y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -23,14 +35,12 @@
   Σ : 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 -∗ Φ #() >>
+                       << ∃ y : val, P y, COMM Φ #() >> >> @ ⊤, ∅
+           << ∃ y : val, P y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -46,11 +56,9 @@
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
-  Q : iPropI Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : Q
-  "AU" : AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Q -∗ Φ #() >>
+  "AU" : AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -59,14 +67,11 @@
   Σ : 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 -∗ Φ #() >>
+              ABORT AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Φ #() >> >> 
+           @ ⊤, ∅ << l ↦ x, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -82,11 +87,9 @@
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
-  Q : iPropI Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : Q
-  "AU" : AU << l ↦ #() >> @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
+  "AU" : AU << l ↦ #() >> @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -95,14 +98,12 @@
   Σ : 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 -∗ Φ #() >>
+                       << ∃ y : val, l ↦ y, COMM Φ #() >> >> @ ⊤, ∅
+           << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -118,11 +119,9 @@
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
-  Q : iPropI Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : Q
-  "AU" : AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Q -∗ Φ #() >>
+  "AU" : AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -131,13 +130,11 @@
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
-  Q : iPropI Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : Q
   _ : AACC << l ↦ #()
-              ABORT AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Q -∗ Φ #() >> >> 
-           @ ⊤, ∅ << l ↦ #(), COMM Q -∗ Φ #() >>
+              ABORT AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Φ #() >> >> 
+           @ ⊤, ∅ << l ↦ #(), COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -155,12 +152,10 @@
   Σ : 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 -∗ Φ #() >>
+            << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -178,12 +173,10 @@
   Σ : 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 -∗ Φ #() >>
+            @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -202,14 +195,12 @@
   Σ : 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 -∗ Φ #() >>
+            COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -227,12 +218,10 @@
   Σ : 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 -∗ Φ #() >>
+            << l ↦ x, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -252,12 +241,10 @@
   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 -∗ Φ #() >>
+            << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -277,12 +264,10 @@
   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 -∗ Φ #() >>
+            << l ↦ #(), COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -302,12 +287,10 @@
   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 -∗ Φ #() >>
+            @ ⊤, ∅ << l ↦ yyyy, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -328,31 +311,16 @@
   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 -∗ Φ #() >>
+               COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
 "Prettification"
      : string
-1 subgoal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  P : val → iProp Σ
-  ============================
-  --------------------------------------∗
-  ∀ Φ : language.val heap_lang → iProp Σ, AU << ∀ 
-                                             x : val, 
-                                             P x >> @ ⊤, ∅
-                                             << ∃ y : val, P y, COMM Φ #() >>
-                                          -∗ WP ! #0 {{ v, Φ v }}
-  
 1 subgoal
   
   Σ : gFunctors
diff --git a/tests/atomic.v b/tests/atomic.v
index 9f2b7dd34229a244f597cbfa719ea7afbe02445a..236ec1e71c6f641b70281fc407182ab11ac2d497 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -1,9 +1,22 @@
 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.
+From iris.heap_lang Require Import proofmode notation atomic_heap.
 Set Default Proof Using "Type".
 
+Section tests.
+  Context `{!heapG Σ} {aheap: atomic_heap Σ}.
+  Import atomic_heap.notation.
+
+  (* FIXME: removing the `val` type annotation breaks printing. *)
+  Lemma test_awp_apply_without (Q : iProp Σ) (l : loc) v :
+    Q -∗ l ↦ v -∗ WP !#l {{ _, Q }}.
+  Proof.
+    iIntros "HQ Hl". awp_apply load_spec without "HQ". Show.
+    iAaccIntro with "Hl"; eauto with iFrame.
+  Qed.
+End tests.
+
 (* Test if AWP and the AU obtained from AWP print. *)
 Section printing.
   Context `{!heapG Σ}.
@@ -13,28 +26,28 @@ Section printing.
   Lemma print_both_quant (P : val → iProp Σ) :
     <<< ∀ x, P x >>> code @ ⊤ <<< ∃ y, P y, RET #() >>>.
   Proof.
-    Show. iIntros (Q Φ) "? AU". Show.
+    Show. iIntros (Φ) "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.
+    Show. iIntros (Φ) "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.
+    Show. iIntros (Φ) "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.
+    Show. iIntros (Φ) "AU". Show.
     iPoseProof (aupd_aacc with "AU") as "?". Show.
   Abort.
 
@@ -43,49 +56,49 @@ Section printing.
   Lemma print_both_quant_long l :
     <<< ∀ x, l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y, l ↦ y, RET #() >>>.
   Proof.
-    Show. iIntros (Q Φ) "? AU". Show.
+    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 #() >>>.
   Proof.
-    Show. iIntros (Q Φ) "? AU". Show.
+    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 #() >>>.
   Proof.
-    Show. iIntros (Q Φ) "? ?". Show.
+    Show. iIntros (Φ) "?". 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.
+    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 #() >>>.
   Proof.
-    Show. iIntros (Q Φ) "? AU". Show.
+    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 #() >>>.
   Proof.
-    Show. iIntros (Q Φ) "? AU". Show.
+    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 #() >>>.
   Proof.
-    Show. iIntros (Q Φ) "? AU". Show.
+    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 #() >>>.
   Proof.
-    Show. iIntros (Q Φ) "? AU". Show.
+    Show. iIntros (Φ) "AU". Show.
   Abort.
 
   Check "Prettification".
@@ -93,7 +106,6 @@ Section printing.
   Lemma iMod_prettify (P : val → iProp Σ) :
     <<< ∀ x, P x >>> !#0 @ ⊤ <<< ∃ y, P y, RET #() >>>.
   Proof.
-    iApply wp_atomic_intro. Show.
     iIntros (Φ) "AU". iMod "AU". Show.
   Abort.
 
diff --git a/theories/heap_lang/lib/atomic_heap.v b/theories/heap_lang/lib/atomic_heap.v
index c88ba0204173197176eec74c2ba60805ad40733c..e5d4804bc6b1a592e9c3f40c5f4084e8725b67b0 100644
--- a/theories/heap_lang/lib/atomic_heap.v
+++ b/theories/heap_lang/lib/atomic_heap.v
@@ -81,18 +81,18 @@ Section proof.
     <<< ∀ (v : val) q, l ↦{q} v >>> primitive_load #l @ ⊤
     <<< l ↦{q} v, RET v >>>.
   Proof.
-    iIntros (Q Φ) "? AU". wp_lam.
+    iIntros (Φ) "AU". wp_lam.
     iMod "AU" as (v q) "[H↦ [_ Hclose]]".
-    wp_load. iMod ("Hclose" with "H↦") as "HΦ". by iApply "HΦ".
+    wp_load. iMod ("Hclose" with "H↦") as "HΦ". done.
   Qed.
 
   Lemma primitive_store_spec (l : loc) (w : val) :
     <<< ∀ v, l ↦ v >>> primitive_store #l w @ ⊤
     <<< l ↦ w, RET #() >>>.
   Proof.
-    iIntros (Q Φ) "? AU". wp_lam. wp_let.
+    iIntros (Φ) "AU". wp_lam. wp_let.
     iMod "AU" as (v) "[H↦ [_ Hclose]]".
-    wp_store. iMod ("Hclose" with "H↦") as "HΦ". by iApply "HΦ".
+    wp_store. iMod ("Hclose" with "H↦") as "HΦ". done.
   Qed.
 
   Lemma primitive_cas_spec (l : loc) (w1 w2 : val) :
@@ -102,10 +102,10 @@ Section proof.
     <<< if decide (v = w1) then l ↦ w2 else l ↦ v,
         RET #(if decide (v = w1) then true else false) >>>.
   Proof.
-    iIntros (? Q Φ) "? AU". wp_lam. wp_let. wp_let.
+    iIntros (? Φ) "AU". wp_lam. wp_let. wp_let.
     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Φ"; done.
   Qed.
 End proof.
 
diff --git a/theories/heap_lang/lib/coin_flip.v b/theories/heap_lang/lib/coin_flip.v
index 885298940c3d118dae418194f590971aa91f7303..57b085436cbc529a968614e52528d67b8272b304 100644
--- a/theories/heap_lang/lib/coin_flip.v
+++ b/theories/heap_lang/lib/coin_flip.v
@@ -50,7 +50,7 @@ Section coinflip.
         @ ⊤
     <<< ∃ (b: bool), x ↦ #0, RET #b >>>.
   Proof.
-    iApply wp_atomic_intro. iIntros (Φ) "AU". wp_lam.
+    iIntros (Φ) "AU". wp_lam.
     wp_apply rand_spec; first done.
     iIntros (b) "_". wp_let.
     wp_bind (_ <- _)%E.
@@ -73,7 +73,7 @@ Section coinflip.
         @ ⊤
     <<< ∃ (b: bool), x ↦ #0, RET #b >>>.
   Proof.
-    iApply wp_atomic_intro. iIntros (Φ) "AU". wp_lam.
+    iIntros (Φ) "AU". wp_lam.
     wp_apply wp_new_proph; first done.
     iIntros (v p) "Hp".
     wp_let.
diff --git a/theories/heap_lang/lib/increment.v b/theories/heap_lang/lib/increment.v
index 6fd0a421562ef871c647f24e336f670a11175a3a..79f600e20796460be3f67970f9e6e9f11fd0b463 100644
--- a/theories/heap_lang/lib/increment.v
+++ b/theories/heap_lang/lib/increment.v
@@ -23,7 +23,7 @@ Section increment_physical.
   Lemma incr_phy_spec (l: loc) :
     <<< ∀ (v : Z), l ↦ #v >>> incr_phy #l @ ⊤ <<< l ↦ #(v + 1), RET #v >>>.
   Proof.
-    iApply wp_atomic_intro. iIntros (Φ) "AU". iLöb as "IH". wp_lam.
+    iIntros (Φ) "AU". iLöb as "IH". wp_lam.
     wp_bind (!_)%E. iMod "AU" as (v) "[Hl [Hclose _]]".
     wp_load. iMod ("Hclose" with "Hl") as "AU". iModIntro.
     wp_pures. wp_bind (CAS _ _ _)%E. iMod "AU" as (w) "[Hl Hclose]".
@@ -55,24 +55,24 @@ Section increment.
   Lemma incr_spec_direct (l: loc) :
     <<< ∀ (v : Z), l ↦ #v >>> incr #l @ ⊤ <<< l ↦ #(v + 1), RET #v >>>.
   Proof.
-    iApply wp_atomic_intro. iIntros (Φ) "AU". iLöb as "IH". wp_lam.
-    wp_apply load_spec; first by iAccu.
+    iIntros (Φ) "AU". iLöb as "IH". wp_lam.
+    awp_apply load_spec.
     (* Prove the atomic update for load *)
-    iAuIntro. rewrite /atomic_acc /=. iMod "AU" as (v) "[Hl [Hclose _]]".
+    rewrite /atomic_acc /=. iMod "AU" as (v) "[Hl [Hclose _]]".
     iModIntro. iExists _, _. iFrame "Hl". iSplit.
     { (* abort case *) done. }
-    iIntros "Hl". iMod ("Hclose" with "Hl") as "AU". iIntros "!> _".
+    iIntros "Hl". iMod ("Hclose" with "Hl") as "AU". iModIntro.
     (* Now go on *)
-    wp_apply cas_spec; [done|iAccu|].
+    awp_apply cas_spec; first done.
     (* Prove the atomic update for CAS *)
-    iAuIntro. rewrite /atomic_acc /=. iMod "AU" as (w) "[Hl Hclose]".
+    rewrite /atomic_acc /=. iMod "AU" as (w) "[Hl Hclose]".
     iModIntro. iExists _. iFrame "Hl". iSplit.
     { (* abort case *) iDestruct "Hclose" as "[? _]". done. }
     iIntros "Hl". destruct (decide (#w = #v)) as [[= ->]|Hx].
     - iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hl") as "HΦ".
-      iIntros "!> _". wp_if. by iApply "HΦ".
+      iIntros "!>". wp_if. by iApply "HΦ".
     - iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "Hl") as "AU".
-      iIntros "!> _". wp_if. iApply "IH". done.
+      iIntros "!>". wp_if. iApply "IH". done.
   Qed.
 
   (** A proof of the incr specification that uses lemmas to avoid reasining
@@ -80,22 +80,22 @@ Section increment.
   Lemma incr_spec (l: loc) :
     <<< ∀ (v : Z), l ↦ #v >>> incr #l @ ⊤ <<< l ↦ #(v + 1), RET #v >>>.
   Proof.
-    iApply wp_atomic_intro. iIntros (Φ) "AU". iLöb as "IH". wp_lam.
-    wp_apply load_spec; first by iAccu.
+    iIntros (Φ) "AU". iLöb as "IH". wp_lam.
+    awp_apply load_spec.
     (* Prove the atomic update for load *)
-    iAuIntro. iApply (aacc_aupd_abort with "AU"); first done.
+    iApply (aacc_aupd_abort with "AU"); first done.
     iIntros (x) "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
-    iIntros "$ !> AU !> _".
+    iIntros "$ !> AU !>".
     (* Now go on *)
-    wp_apply cas_spec; [done|iAccu|].
+    awp_apply cas_spec; first done.
     (* Prove the atomic update for CAS *)
-    iAuIntro. iApply (aacc_aupd with "AU"); first done.
+    iApply (aacc_aupd with "AU"); first done.
     iIntros (x') "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
     iIntros "H↦ !>".
     destruct (decide (#x' = #x)) as [[= ->]|Hx].
-    - iRight. iFrame. iIntros "HΦ !> _".
+    - iRight. iFrame. iIntros "HΦ !>".
       wp_if. by iApply "HΦ".
-    - iLeft. iFrame. iIntros "AU !> _".
+    - iLeft. iFrame. iIntros "AU !>".
       wp_if. iApply "IH". done.
   Qed.
 
@@ -116,17 +116,17 @@ Section increment.
       weak_incr #l @ ⊤
     <<< ⌜v = v'⌝ ∗ l ↦ #(v + 1), RET #v >>>.
   Proof.
-    iIntros "Hl". iApply wp_atomic_intro. iIntros (Φ) "AU". wp_lam.
+    iIntros "Hl" (Φ) "AU". wp_lam.
     wp_apply (atomic_wp_seq $! (load_spec _) with "Hl").
-    iIntros "Hl". wp_apply store_spec; first by iAccu.
+    iIntros "Hl". awp_apply store_spec.
     (* Prove the atomic update for store *)
-    iAuIntro. iApply (aacc_aupd_commit with "AU"); first done.
+    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.
+    iIntros "HΦ !>". wp_seq. done.
   Qed.
 
 End increment.
@@ -149,8 +149,8 @@ Section increment_client.
     (* 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 #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.
+    { iAlways. awp_apply incr_spec. clear x.
+      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/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 05eb1b56e759f5c1c5c787e33212a2640711f028..92851e21392ece4904ec055e61f96694d512e84e 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -1,4 +1,5 @@
 From iris.program_logic Require Export weakestpre total_weakestpre.
+From iris.program_logic Require Import atomic.
 From iris.proofmode Require Import coq_tactics reduction.
 From iris.proofmode Require Export tactics.
 From iris.heap_lang Require Export tactics lifting.
@@ -354,24 +355,40 @@ Proof.
 Qed.
 End heap.
 
-Tactic Notation "wp_apply" open_constr(lem) :=
+(** Evaluate [lem] to a hypothesis [H] that can be applied, and then run
+[wp_bind K; tac H] for every possible evaluation context.  [tac] can do
+[iApplyHyp H] to actually apply the hypothesis.  TC resolution of [lem] premises
+happens *after* [tac H] got executed. *)
+Tactic Notation "wp_apply_core" open_constr(lem) tactic(tac) :=
   wp_pures;
   iPoseProofCore lem as false true (fun H =>
     lazymatch goal with
     | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
       reshape_expr e ltac:(fun K e' =>
-        wp_bind_core K; iApplyHyp H; try iNext; try wp_expr_simpl) ||
+        wp_bind_core K; tac H) ||
       lazymatch iTypeOf H with
       | Some (_,?P) => fail "wp_apply: cannot apply" P
       end
     | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
       reshape_expr e ltac:(fun K e' =>
-        twp_bind_core K; iApplyHyp H; try wp_expr_simpl) ||
+        twp_bind_core K; tac H) ||
       lazymatch iTypeOf H with
       | Some (_,?P) => fail "wp_apply: cannot apply" P
       end
     | _ => fail "wp_apply: not a 'wp'"
     end).
+Tactic Notation "wp_apply" open_constr(lem) :=
+  wp_apply_core lem (fun H => iApplyHyp H; try iNext; try wp_expr_simpl).
+(** Tactic tailored for atomic triples: the first, simple one just runs
+[iAuIntro] on the goal, as atomic triples always have an atomic update as their
+premise.  The second one additionaly does some framing: it gets rid of [Hs] from
+the context, which is intended to be the non-laterable assertions that iAuIntro
+would choke on.  You get them all back in the continuation of the atomic
+operation. *)
+Tactic Notation "awp_apply" open_constr(lem) :=
+  wp_apply_core lem (fun H => iApplyHyp H; last iAuIntro).
+Tactic Notation "awp_apply" open_constr(lem) "without" constr(Hs) :=
+  wp_apply_core lem (fun H => iApply wp_frame_wand_l; iSplitL Hs; [iAccu|iApplyHyp H; last iAuIntro]).
 
 Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
   let Htmp := iFresh in
diff --git a/theories/program_logic/atomic.v b/theories/program_logic/atomic.v
index 9c0df10983a554c10c2b9b16c4c756827cdbca3d..25df772be33d0ef798f62fb779f4a33050d1a96c 100644
--- a/theories/program_logic/atomic.v
+++ b/theories/program_logic/atomic.v
@@ -14,8 +14,8 @@ Definition atomic_wp `{irisG Λ Σ} {TA TB : tele}
   (β: TA → TB → iProp Σ) (* atomic post-condition *)
   (f: TA → TB → val Λ) (* Turn the return data into the return value *)
   : iProp Σ :=
-    (∀ Q (Φ : val Λ → iProp Σ), Q -∗
-             atomic_update Eo ∅ α β (λ.. x y, Q -∗ Φ (f x y)) -∗
+    (∀ (Φ : val Λ → iProp Σ),
+             atomic_update Eo ∅ α β (λ.. x y, Φ (f x y)) -∗
              WP e {{ Φ }})%I.
 (* Note: To add a private postcondition, use
    atomic_update α β Eo Ei (λ x y, POST x y -∗ Φ (f x y)) *)
@@ -102,8 +102,8 @@ Section lemmas.
     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.
+    rewrite ->tforall_forall in HL. iIntros "Hwp" (Φ x) "Hα HΦ".
+    iApply wp_frame_wand_l. iSplitL "HΦ"; first iAccu. iApply "Hwp".
     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.
@@ -116,23 +116,12 @@ Section lemmas.
     (∀ Φ, ∀.. 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.
+    simpl in HP. iIntros "Hwp" (Φ) "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.
+    rewrite ->!tele_app_bind. 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.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 92ddffd1616eac02a9e906c36d9fbe860695fdbe..65513253b663208b17b632dbc092cc29273903ad 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -241,6 +241,13 @@ Proof. iIntros "[H Hwp]". iApply (wp_wand with "Hwp H"). Qed.
 Lemma wp_wand_r s E e Φ Ψ :
   WP e @ s; E {{ Φ }} ∗ (∀ v, Φ v -∗ Ψ v) ⊢ WP e @ s; E {{ Ψ }}.
 Proof. iIntros "[Hwp H]". iApply (wp_wand with "Hwp H"). Qed.
+Lemma wp_frame_wand_l s E e Q Φ :
+  Q ∗ WP e @ s; E {{ v, Q -∗ Φ v }} -∗ WP e @ s; E {{ Φ }}.
+Proof.
+  iIntros "[HQ HWP]". iApply (wp_wand with "HWP").
+  iIntros (v) "HΦ". by iApply "HΦ".
+Qed.
+
 End wp.
 
 (** Proofmode class instances *)