diff --git a/theories/typing/types.v b/theories/typing/types.v
index 3426ea5c726a1e4c86584adb8635dd276c18388c..c466404b6f3d3a8bc3683d7d3d967962a7d8ca4b 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -68,7 +68,7 @@ Reserved Notation "Γ ⊢ₜ e : τ" (at level 74, e, τ at next level).
 
 (** We model type-level lambdas and applications as thunks *)
 Notation "Λ: e" := (λ: <>, e)%E (at level 200).
-Notation "'TApp' e" := (e #())%E (at level 200).
+Notation "'TApp' e" := (App e%E #()%E) (at level 200).
 
 (* To unfold a recursive type, we need to take a step. We thus define the
 unfold operator to be the identity function. *)