diff --git a/coq/smallstep.v b/coq/smallstep.v
index 63f1cc1..2a88c99 100644
--- a/coq/smallstep.v
+++ b/coq/smallstep.v
@@ -65,38 +65,16 @@ Inductive beta_step : expr_term -> expr_term -> Prop :=
     (expr_ty_app (expr_ty_abs x e) a) -->β (expr_specialize x a e)
 
   | E_AppLam : forall x τ e a,
-    (expr_tm_app (expr_tm_abs x τ e) a) -->β (expr_subst x a e)
+    (expr_app (expr_abs x τ e) a) -->β (expr_subst x a e)
+
+  | E_AppMorph : forall x τ e a,
+    (expr_app (expr_morph x τ e) a) -->β (expr_subst x a e)
 
   | E_AppLet : forall x t e a,
     (expr_let x t a e) -->β (expr_subst x a e)
 
 where "s '-->β' t" := (beta_step s t).
 
-
-
-Inductive delta_step : expr_term -> expr_term -> Prop :=
-
-  | E_ImplicitCast : forall (Γ:context) (f:expr_term) (h:string) (a:expr_term) (τ:type_term) (s:type_term) (p:type_term),
-
-    (context_contains Γ h (type_morph p s)) ->
-    Γ |- f \is (type_fun s τ) ->
-    Γ |- a \is p ->
-    (expr_tm_app f a) -->δ (expr_tm_app f (expr_tm_app (expr_var h) a))
-
-where "s '-->δ' t" := (delta_step s t).
-
-
-Inductive eval_step : expr_term -> expr_term -> Prop :=
-  | E_Beta : forall s t,
-    (s -->β t) ->
-    (s -->eval t)
-
-  | E_Delta : forall s t,
-    (s -->δ t) ->
-    (s -->eval t)
-
-where "s '-->eval' t" := (eval_step s t).
-
 Inductive multi {X : Type} (R : X -> X -> Prop) : X -> X -> Prop :=
   | Multi_Refl : forall (x : X), multi R x x
   | Multi_Step : forall (x y z : X),