diff --git a/coq/terms.v b/coq/terms.v
index 3cc59aa..a48ff29 100644
--- a/coq/terms.v
+++ b/coq/terms.v
@@ -98,11 +98,20 @@ Notation "[{ e }]" := e
   (e custom ladder_expr at level 80) : ladder_expr_scope.
 Notation "'%' x '%'" := (expr_var x%string)
   (in custom ladder_expr at level 0, x constr) : ladder_expr_scope.
-Notation "'λ' x τ '↦' e" := (expr_abs x τ e) (in custom ladder_expr at level 0, x constr, τ custom ladder_type at level 99, e custom ladder_expr at level 99).
 Notation "'Λ' t '↦' e" := (expr_ty_abs t e)
-  (in custom ladder_expr at level 0, t constr, e custom ladder_expr at level 80).
-
-
+  (in custom ladder_expr at level 10, t constr, e custom ladder_expr at level 80) : ladder_expr_scope.
+Notation "'λ' x τ '↦' e" := (expr_abs x τ e)
+  (in custom ladder_expr at level 10, x constr, τ custom ladder_type at level 99, e custom ladder_expr at level 99) :ladder_expr_scope.
+Notation "'λ' x τ '↦morph' e" := (expr_morph x τ e)
+  (in custom ladder_expr at level 10, x constr, τ custom ladder_type at level 99, e custom ladder_expr at level 99) :ladder_expr_scope.
+Notation "'let' x ':=' e 'in' t" := (expr_let x e t)
+  (in custom ladder_expr at level 20, x constr, e custom ladder_expr at level 99, t custom ladder_expr at level 99) : ladder_expr_scope.
+Notation "e 'as' τ" := (expr_ascend τ e)
+  (in custom ladder_expr at level 30, e custom ladder_expr, τ custom ladder_type at level 99) : ladder_expr_scope.
+Notation "e1 e2" := (expr_app e1 e2)
+  (in custom ladder_expr at level 50) : ladder_expr_scope.
+Notation "'(' e ')'" := e
+  (in custom ladder_expr at level 0) : ladder_expr_scope.
 
 (* EXAMPLES *)
 
@@ -111,7 +120,7 @@ Open Scope ladder_expr_scope.
 
 Check [< ∀"α", (< $"Seq"$ %"α"% > ~ < $"List"$ %"α"% >) >].
 
-Definition polymorphic_identity1 : expr_term := [{ Λ"T" ↦ λ"x"%"T"% ↦ %"x"% }].
+Definition polymorphic_identity1 : expr_term := [{ Λ"T" ↦ λ"x"%"T"% ↦ (%"x"%) }].
 Definition polymorphic_identity2 : expr_term := [{ Λ"T" ↦ λ"y"%"T"% ↦ %"y"% }].
 
 Compute polymorphic_identity1.