diff --git a/theories/program_logic/atomic.v b/theories/program_logic/atomic.v
index 487acd3567c327b27d4fdaf44c1799c56f605a39..847f2705c4e62060a7deda32e7ee79a3476eec51 100644
--- a/theories/program_logic/atomic.v
+++ b/theories/program_logic/atomic.v
@@ -112,8 +112,8 @@ Section lemmas.
   (* 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 {{ Φ }}) -∗
+        (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.
   Proof.
     simpl in HP. iIntros "Hwp" (Φ) "HΦ". iApply fupd_wp.