diff --git a/src/plfa/part2/More.lagda.md b/src/plfa/part2/More.lagda.md
index 2259d5cf..74b5c1d3 100644
--- a/src/plfa/part2/More.lagda.md
+++ b/src/plfa/part2/More.lagda.md
@@ -1105,9 +1105,9 @@ data Finished {Γ A} (N : Γ ⊢ A) : Set where
        ----------
        Finished N
 
-data Steps : ∀ {A} → ∅ ⊢ A → Set where
+data Steps {A} : ∅ ⊢ A → Set where
 
-  steps : ∀ {A} {L N : ∅ ⊢ A}
+  steps : {L N : ∅ ⊢ A}
     → L —↠ N
     → Finished N
       ----------