diff --git a/coq/_CoqProject b/coq/_CoqProject
index 5f61850..139d674 100644
--- a/coq/_CoqProject
+++ b/coq/_CoqProject
@@ -12,8 +12,10 @@ subtype_debruijn.v
 context_debruijn.v
 morph_debruijn.v
 typing_debruijn.v
+eval_debruijn.v
 subst_lemmas_debruijn.v
 
+
 terms.v
 equiv.v
 subst.v
diff --git a/coq/eval_debruijn.v b/coq/eval_debruijn.v
new file mode 100644
index 0000000..b86631d
--- /dev/null
+++ b/coq/eval_debruijn.v
@@ -0,0 +1,77 @@
+From Coq Require Import Lists.List.
+Import ListNotations.
+Require Import Atom.
+Require Import terms_debruijn.
+Require Import subtype_debruijn.
+Require Import context_debruijn.
+Require Import morph_debruijn.
+Require Import typing_debruijn.
+
+Open Scope ladder_expr_scope.
+
+Inductive is_value : expr_DeBruijn -> Prop :=
+  | V_TAbs : forall e,
+    is_value [{ Λ e }]
+
+  | V_Abs : forall σ e,
+    is_value [{ λ σ ↦ e }]
+
+  | V_Morph : forall σ e,
+    is_value [{ λ σ ↦morph e }]
+
+  | V_Ascend : forall τ e,
+    is_value e ->
+    is_value [{ e as τ }]
+
+  | V_Descend : forall τ e,
+    is_value e ->
+    is_value [{ e des τ }]
+.
+
+
+Reserved Notation " s '-->eval' t " (at level 40).
+
+Inductive eval : expr_DeBruijn -> expr_DeBruijn -> Prop :=
+  | E_App1 : forall e1 e1' e2,
+    e1 -->eval e1' ->
+    [{ e1 e2 }] -->eval [{ e1' e2 }]
+
+  | E_App2 : forall v1 e2 e2',
+    (is_value v1) ->
+    e2 -->eval e2' ->
+    [{ v1 e2 }] -->eval [{ v1 e2' }]
+
+  | E_TypApp : forall e e',
+    e -->eval e' ->
+    [{ Λ e }] -->eval [{ Λ e' }]
+
+  | E_TypAppLam : forall e τ,
+    [{ (Λ e) # τ }] -->eval (expr_open_type τ e)
+
+  | E_AppLam : forall τ e a,
+    [{ (λ τ ↦ e) a }] -->eval (expr_open a e)
+
+  | E_AppMorph : forall τ e a,
+    [{ (λ τ ↦morph e) a }] -->eval (expr_open a e)
+
+  | E_Let : forall e a,
+    [{ let a in e }] -->eval (expr_open a e)
+
+  | E_StripAscend : forall τ e,
+    [{ e as τ }] -->eval e
+
+  | E_StripDescend : forall τ e,
+    [{ e des τ }] -->eval e
+
+  | E_Ascend : forall τ e e',
+    (e -->eval e') ->
+    [{ e as τ }] -->eval [{ e' as τ }]
+
+  | E_AscendCollapse : forall τ' τ e,
+    [{ (e as τ) as τ' }] -->eval [{ e as (τ'~τ) }]
+
+  | E_DescendCollapse : forall τ' τ e,
+    (τ':<=τ) ->
+    [{ (e des τ') des τ }] -->eval [{ e des τ }]
+
+where "s '-->eval' t" := (eval s t).