diff --git a/coq/smallstep.v b/coq/smallstep.v
index 067678c..63f1cc1 100644
--- a/coq/smallstep.v
+++ b/coq/smallstep.v
@@ -52,9 +52,10 @@ Inductive beta_step : expr_term -> expr_term -> Prop :=
     e1 -->β e1' ->
     (expr_app e1 e2) -->β (expr_app e1' e2)
 
-  | E_App2 : forall e1 e2 e2',
+  | E_App2 : forall v1 e2 e2',
+    (is_value v1) ->
     e2 -->β e2' ->
-    (expr_app e1 e2) -->β (expr_app e1 e2')
+    (expr_app v1 e2) -->β (expr_app v1 e2')
 
   | E_TypApp : forall e e' τ,
     e -->β e' ->