diff --git a/coq/subst.v b/coq/subst.v
index 74e586c..1f2b0c8 100644
--- a/coq/subst.v
+++ b/coq/subst.v
@@ -23,6 +23,7 @@ Fixpoint expr_subst (v:string) (n:expr_term) (e0:expr_term) :=
   | expr_ty_abs x e => if (eqb v x) then e0 else expr_ty_abs x (expr_subst v n e)
   | expr_ty_app e t => expr_ty_app (expr_subst v n e) t
   | expr_tm_abs x t e => if (eqb v x) then e0 else expr_tm_abs x t (expr_subst v n e)
+  | expr_tm_abs_morph x t e => if (eqb v x) then e0 else expr_tm_abs_morph x t (expr_subst v n e)
   | expr_tm_app e a => expr_tm_app (expr_subst v n e) (expr_subst v n a)
   | expr_let x t a e => expr_let x t (expr_subst v n a) (expr_subst v n e)
   | expr_ascend t e => expr_ascend t (expr_subst v n e)
diff --git a/coq/terms.v b/coq/terms.v
index de2217d..1930840 100644
--- a/coq/terms.v
+++ b/coq/terms.v
@@ -15,6 +15,7 @@ Inductive type_term : Type :=
   | type_fun : type_term -> type_term -> type_term
   | type_univ : string -> type_term -> type_term
   | type_spec : type_term -> type_term -> type_term
+  | type_morph : type_term -> type_term -> type_term
   | type_ladder : type_term -> type_term -> type_term
 .
 
@@ -24,6 +25,7 @@ Inductive expr_term : Type :=
   | expr_ty_abs : string -> expr_term -> expr_term
   | expr_ty_app : expr_term -> type_term -> expr_term
   | expr_tm_abs : string -> type_term -> expr_term -> expr_term
+  | expr_tm_abs_morph : string -> type_term -> expr_term -> expr_term
   | expr_tm_app : expr_term -> expr_term -> expr_term
   | expr_let : string -> type_term -> expr_term -> expr_term -> expr_term
   | expr_ascend : type_term -> expr_term -> expr_term