diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 28a52c0e56bba92acff74ac66f49cc3693522477..f2b6d69e7dc6255505857a9f3bb8be0c2721f1a3 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -82,7 +82,7 @@ End typing.
 Notation typed_instruction_ty E L T e ty :=
   (typed_instruction E L T e (λ v : val, [v ◁ ty%list%T]%TC)).
 
-Notation typed_val e ty := (∀ E L, typed_instruction_ty E L [] e ty).
+Notation typed_val v ty := (∀ E L, typed_instruction_ty E L [] (of_val v) ty).
 
 Section typing_rules.
   Context `{typeG Σ}.