diff --git a/LambdaCalculusAndTypeSoundness.v b/LambdaCalculusAndTypeSoundness.v
index 05a2adf..66e9c20 100644
--- a/LambdaCalculusAndTypeSoundness.v
+++ b/LambdaCalculusAndTypeSoundness.v
@@ -312,7 +312,7 @@ Module Ulc.
 
   (* Function application (called "beta reduction") is the big rule here. *)
   Inductive step : exp -> exp -> Prop :=
-  | ContextBeta : forall x e v,
+  | Beta : forall x e v,
     value v
     -> step (App (Abs x e) v) (subst v x e)
 
diff --git a/LambdaCalculusAndTypeSoundness_template.v b/LambdaCalculusAndTypeSoundness_template.v
index ef200c1..8950521 100644
--- a/LambdaCalculusAndTypeSoundness_template.v
+++ b/LambdaCalculusAndTypeSoundness_template.v
@@ -279,7 +279,7 @@ Module Ulc.
   (** * Small-step semantics *)
 
   Inductive step : exp -> exp -> Prop :=
-  | ContextBeta : forall x e v,
+  | Beta : forall x e v,
     value v
     -> step (App (Abs x e) v) (subst v x e)