diff --git a/coq/morph.v b/coq/morph.v
index 01ea18c..8b7855c 100644
--- a/coq/morph.v
+++ b/coq/morph.v
@@ -30,6 +30,10 @@ Inductive morphism_path : context -> type_term -> type_term -> Prop :=
     (Γ |- τ' ~> τ'') ->
     (Γ |- τ ~> τ'')
 
+  | M_Lift : forall Γ σ τ τ',
+    (Γ |- τ ~> τ') ->
+    (Γ |- (type_ladder σ τ) ~> (type_ladder σ τ'))
+
   | M_MapSeq : forall Γ τ τ',
     (Γ |- τ ~> τ') ->
     (Γ |- (type_spec (type_id "Seq") τ) ~> (type_spec (type_id "Seq") τ'))