diff --git a/theories/heap_lang/lib/coin_flip.v b/theories/heap_lang/lib/coin_flip.v
index 57b085436cbc529a968614e52528d67b8272b304..7e3569b1eb12564cb7d097c37992a63ecffeb34e 100644
--- a/theories/heap_lang/lib/coin_flip.v
+++ b/theories/heap_lang/lib/coin_flip.v
@@ -1,7 +1,7 @@
 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 par.
+From iris.heap_lang Require Import proofmode notation.
 Set Default Proof Using "Type".
 
 (** Nondeterminism and Speculation:
diff --git a/theories/heap_lang/lib/par.v b/theories/heap_lang/lib/par.v
index 0d55d3a4b748c9fd06a99b9cba7e2f7840593c59..34c6ad2e72d8ce9ba34a964d5708efe0e20a98e8 100644
--- a/theories/heap_lang/lib/par.v
+++ b/theories/heap_lang/lib/par.v
@@ -12,8 +12,6 @@ Definition par : val :=
     let: "v1" := join "handle" in
     ("v1", "v2").
 Notation "e1 ||| e2" := (par (λ: <>, e1)%E (λ: <>, e2)%E) : expr_scope.
-(* Not a value itself, but with *unlocked* value lambdas. *)
-Local Notation "e1 ||| e2" := (par (LamV BAnon e1%E) (LamV BAnon e2%E)) : val_scope.
 
 Section proof.
 Local Set Default Proof Using "Type*".
@@ -39,7 +37,7 @@ Qed.
 Lemma wp_par (Ψ1 Ψ2 : val → iProp Σ) (e1 e2 : expr) (Φ : val → iProp Σ) :
   WP e1 {{ Ψ1 }} -∗ WP e2 {{ Ψ2 }} -∗
   (∀ v1 v2, Ψ1 v1 ∗ Ψ2 v2 -∗ ▷ Φ (v1,v2)%V) -∗
-  WP (e1 ||| e2)%V {{ Φ }}.
+  WP par (LamV BAnon e1) (LamV BAnon e2) {{ Φ }}.
 Proof.
   iIntros "H1 H2 H".
   wp_apply (par_spec Ψ1 Ψ2 with "[H1] [H2] [H]"); [by wp_lam..|auto].