diff --git a/src/plfa/part2/DeBruijn.lagda.md b/src/plfa/part2/DeBruijn.lagda.md
index 9b94d5ff..eb07df41 100644
--- a/src/plfa/part2/DeBruijn.lagda.md
+++ b/src/plfa/part2/DeBruijn.lagda.md
@@ -874,13 +874,13 @@ infix  1 begin_
 infixr 2 _—→⟨_⟩_
 infix  3 _∎
 
-data _—↠_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
+data _—↠_ {Γ A} : (Γ ⊢ A) → (Γ ⊢ A) → Set where
 
-  _∎ : ∀ {Γ A} (M : Γ ⊢ A)
+  _∎ : (M : Γ ⊢ A)
       ------
     → M —↠ M
 
-  _—→⟨_⟩_ : ∀ {Γ A} (L : Γ ⊢ A) {M N : Γ ⊢ A}
+  _—→⟨_⟩_ : (L : Γ ⊢ A) {M N : Γ ⊢ A}
     → L —→ M
     → M —↠ N
       ------
diff --git a/src/plfa/part2/More.lagda.md b/src/plfa/part2/More.lagda.md
index 74b5c1d3..548ad58a 100644
--- a/src/plfa/part2/More.lagda.md
+++ b/src/plfa/part2/More.lagda.md
@@ -989,13 +989,13 @@ infix  1 begin_
 infixr 2 _—→⟨_⟩_
 infix  3 _∎
 
-data _—↠_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
+data _—↠_ {Γ A} : (Γ ⊢ A) → (Γ ⊢ A) → Set where
 
-  _∎ : ∀ {Γ A} (M : Γ ⊢ A)
+  _∎ : (M : Γ ⊢ A)
       ------
     → M —↠ M
 
-  _—→⟨_⟩_ : ∀ {Γ A} (L : Γ ⊢ A) {M N : Γ ⊢ A}
+  _—→⟨_⟩_ : (L : Γ ⊢ A) {M N : Γ ⊢ A}
     → L —→ M
     → M —↠ N
       ------