diff --git a/coq/terms.v b/coq/terms.v
index 00c075d..2ae8d33 100644
--- a/coq/terms.v
+++ b/coq/terms.v
@@ -65,6 +65,8 @@ Declare Custom Entry ladder_expr.
 
 Notation "[< t >]" := t
   (t custom ladder_type at level 80) : ladder_type_scope.
+Notation "t" := t
+  (in custom ladder_type at level 0, t ident) : ladder_type_scope.
 Notation "'∀' x ',' t" := (type_univ x t)
   (t custom ladder_type at level 80, in custom ladder_type at level 80, x constr).
 Notation "'<' σ τ '>'" := (type_spec σ τ)
@@ -84,6 +86,8 @@ Notation "'%' x '%'" := (type_var x%string)
 
 Notation "[{ e }]" := e
   (e custom ladder_expr at level 80) : ladder_expr_scope.
+Notation "e" := e
+  (in custom ladder_expr at level 0, e ident) : ladder_expr_scope.
 Notation "'%' x '%'" := (expr_var x%string)
   (in custom ladder_expr at level 0, x constr) : ladder_expr_scope.
 Notation "'Λ' t '↦' e" := (expr_ty_abs t e)