diff --git a/coq/terms_debruijn.v b/coq/terms_debruijn.v
index 1e7706f..de643ed 100644
--- a/coq/terms_debruijn.v
+++ b/coq/terms_debruijn.v
@@ -27,11 +27,66 @@ Inductive expr_DeBruijn : Type :=
   | ex_abs   : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
   | ex_morph : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
   | ex_app : expr_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
-  | ex_let : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
+  | ex_let : expr_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
   | ex_ascend : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
   | ex_descend : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
 .
 
+Declare Scope ladder_type_scope.
+Declare Scope ladder_expr_scope.
+Declare Custom Entry ladder_type.
+Declare Custom Entry ladder_expr.
+
+Notation "[< t >]" := t
+  (t custom ladder_type at level 99) : ladder_type_scope.
+Notation "t" := t
+  (in custom ladder_type at level 0, t ident) : ladder_type_scope.
+Notation "'∀' t" := (ty_univ t)
+  (t custom ladder_type at level 80, in custom ladder_type at level 80).
+Notation "'<' σ τ '>'" := (ty_spec σ τ)
+  (in custom ladder_type at level 80, left associativity) : ladder_type_scope.
+Notation "'[' τ ']'" := (ty_spec (ty_id "Seq") τ)
+  (in custom ladder_type at level 70) : ladder_type_scope.
+Notation "'(' τ ')'" := τ
+  (in custom ladder_type at level 5) : ladder_type_scope.
+Notation "σ '->' τ" := (ty_func σ τ)
+  (in custom ladder_type at level 75, right associativity) : ladder_type_scope.
+Notation "σ '->morph' τ" := (ty_morph σ τ)
+  (in custom ladder_type at level 75, right associativity, τ at level 80) : ladder_type_scope.
+Notation "σ '~' τ" := (ty_ladder σ τ)
+  (in custom ladder_type at level 20, right associativity) : ladder_type_scope.
+Notation "'$' x" := (ty_id x%string)
+  (in custom ladder_type at level 10, x constr) : ladder_type_scope.
+Notation "'%' x" := (ty_fvar x)
+  (in custom ladder_type at level 10, x constr) : ladder_type_scope.
+
+Notation "[{ e }]" := e
+  (e custom ladder_expr at level 99) : ladder_expr_scope.
+Notation "e" := e
+  (in custom ladder_expr at level 0, e ident) : ladder_expr_scope.
+Notation "'$' x" := (ex_fvar x)
+  (in custom ladder_expr at level 10, x constr) : ladder_expr_scope.
+Notation "'%' x" := (ex_bvar x)
+  (in custom ladder_expr at level 10, x constr) : ladder_expr_scope.
+Notation "'Λ' e" := (ex_ty_abs e)
+  (in custom ladder_expr at level 10, e custom ladder_expr at level 80, right associativity) : ladder_expr_scope.
+Notation "'λ' τ '↦' e" := (ex_abs τ e)
+  (in custom ladder_expr at level 70, τ custom ladder_type at level 90, e custom ladder_expr at level 80, right associativity) :ladder_expr_scope.
+Notation "'λ' τ '↦morph' e" := (ex_morph τ e)
+  (in custom ladder_expr at level 70, τ custom ladder_type at level 90, e custom ladder_expr at level 80, right associativity) :ladder_expr_scope.
+Notation "'let' e 'in' t" := (ex_let e t)
+  (in custom ladder_expr at level 60, e custom ladder_expr at level 80, t custom ladder_expr at level 80, right associativity) : ladder_expr_scope.
+Notation "e 'as' τ" := (ex_ascend τ e)
+  (in custom ladder_expr at level 30, e custom ladder_expr, τ custom ladder_type at level 99) : ladder_expr_scope.
+Notation "e 'des' τ" := (ex_descend τ e)
+  (in custom ladder_expr at level 30, e custom ladder_expr, τ custom ladder_type at level 99) : ladder_expr_scope.
+Notation "e1 e2" := (ex_app e1 e2)
+  (in custom ladder_expr at level 90, e2 custom ladder_expr at next level) : ladder_expr_scope.
+Notation "e '#' τ" := (ex_ty_app e τ)
+  (in custom ladder_expr at level 80, τ custom ladder_type at level 101, left associativity) : ladder_expr_scope.
+Notation "'(' e ')'" := e
+  (in custom ladder_expr, e custom ladder_expr at next level, left associativity) : ladder_expr_scope.
+
 (* get the list of all free variables in a type term *)
 Fixpoint type_fv (τ : type_DeBruijn) {struct τ} : atoms :=
   match τ with