diff --git a/coq/terms/debruijn.v b/coq/terms/debruijn.v
index 54a6cdb..1c78ef0 100644
--- a/coq/terms/debruijn.v
+++ b/coq/terms/debruijn.v
@@ -280,8 +280,12 @@ Inductive expr_lc : expr_DeBruijn -> Prop :=
       (type_lc σ) ->
       (forall x, (x `notin` L) -> expr_lc (expr_open (ex_fvar x) e1)) ->
       expr_lc (ex_abs σ e1)
-  | Tlc_App : forall e1 e2, expr_lc e1 -> expr_lc e2 -> expr_lc (ex_app e1 e2)
-  | Tlc_Let : forall e1 e2, expr_lc e1 -> expr_lc e2 -> expr_lc (ex_let e1 e2)
-  | Tlc_Ascend : forall τ e, type_lc τ -> expr_lc e -> expr_lc (ex_ascend τ e)
-  | Tlc_Descend : forall τ e, type_lc τ -> expr_lc e -> expr_lc (ex_descend τ e)
+  | Elc_Morph : forall σ e1 L,
+      (type_lc σ) ->
+      (forall x, (x `notin` L) -> expr_lc (expr_open (ex_fvar x) e1)) ->
+      expr_lc (ex_morph σ e1)
+  | Elc_App : forall e1 e2, expr_lc e1 -> expr_lc e2 -> expr_lc (ex_app e1 e2)
+  | Elc_Let : forall e1 e2, expr_lc e1 -> expr_lc e2 -> expr_lc (ex_let e1 e2)
+  | Elc_Ascend : forall τ e, type_lc τ -> expr_lc e -> expr_lc (ex_ascend τ e)
+  | Elc_Descend : forall τ e, type_lc τ -> expr_lc e -> expr_lc (ex_descend τ e)
 .