diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3867278c6c..80fe780134 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -42,6 +42,9 @@ Non-backwards compatible changes
 Minor improvements
 ------------------
 
+* In `Induction.WellFoudned`, the final parameter of `Acc` has been changed to
+  an index.
+
 Deprecated modules
 ------------------
 
diff --git a/src/Induction/WellFounded.agda b/src/Induction/WellFounded.agda
index 4d5aec6a74..f84ff2c098 100644
--- a/src/Induction/WellFounded.agda
+++ b/src/Induction/WellFounded.agda
@@ -43,8 +43,8 @@ WfRec _<_ P x = ∀ {y} → y < x → P y
 -- The accessibility predicate: x is accessible if everything which is
 -- smaller than x is also accessible (inductively).
 
-data Acc {A : Set a} (_<_ : Rel A ℓ) (x : A) : Set (a ⊔ ℓ) where
-  acc : (rs : WfRec _<_ (Acc _<_) x) → Acc _<_ x
+data Acc {A : Set a} (_<_ : Rel A ℓ) : (x : A) → Set (a ⊔ ℓ) where
+  acc : ∀ {x} (rs : WfRec _<_ (Acc _<_) x) → Acc _<_ x
 
 -- The accessibility predicate encodes what it means to be
 -- well-founded; if all elements are accessible, then _<_ is