diff --git a/HeapLang.md b/HeapLang.md
index 0ac3a23b94776714c0537cc66155bc46b9251e56..b9f2cd1125a93051a0cf83671ec31b8d1db55d9b 100644
--- a/HeapLang.md
+++ b/HeapLang.md
@@ -117,11 +117,11 @@ The normal `e1 ||| e2` notation uses expression lambdas, because clearly we want
value lambda). However, the *specification* for parallel composition should use
value lambdas, because prior to applying it the term will be reduced as much as
possible to achieve a normal form. To facilitate this, we define a copy of the
-`e1 ||| e2` notation in the value scope that uses value lambdas. This is not
-actually a value, but we still but it in the value scope to differentiate from
-the other notation that uses expression lambdas. (In the future, we might
-decide to add a separate scope for this.) Then, we write the canonical
-specification using the notation in the value scope.
+`e1 ||| e2` notation in the value scope that uses *unlocked* value lambdas.
+This is not actually a value, but we still but it in the value scope to
+differentiate from the other notation that uses expression lambdas. (In the
+future, we might decide to add a separate scope for this.) Then, we write the
+canonical specification using the notation in the value scope.
This works very well for non-recursive notions. For `while` loops, the
situation is unfortunately more complex and proving the desired specification
diff --git a/theories/heap_lang/lib/par.v b/theories/heap_lang/lib/par.v
index 558853f4f48d15d4eae8f61cffd88981686e4abd..d073142e287b92261be068832504c3cc3715b442 100644
--- a/theories/heap_lang/lib/par.v
+++ b/theories/heap_lang/lib/par.v
@@ -12,7 +12,7 @@ Definition par : val :=
let: "v1" := join "handle" in
("v1", "v2").
Notation "e1 ||| e2" := (par (λ: <>, e1)%E (λ: <>, e2)%E) : expr_scope.
-Notation "e1 ||| e2" := (par (λ: <>, e1)%V (λ: <>, e2)%V) : val_scope.
+Notation "e1 ||| e2" := (par (LamV BAnon e1%E) (LamV BAnon e2%E)) : val_scope.
Section proof.
Local Set Default Proof Using "Type*".