diff --git a/src/Lean/Elab/PreDefinition/WF/Fix.lean b/src/Lean/Elab/PreDefinition/WF/Fix.lean
index 3b878af7756d..e52adb048ff9 100644
--- a/src/Lean/Elab/PreDefinition/WF/Fix.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Fix.lean
@@ -188,8 +188,9 @@ def assignSubsumed (mvars : Array MVarId) : MetaM (Array MVarId) :=
     return (true, true)
 
 /--
-The subgoals are of the form `rel arg param`, where `param` is the `PackMutual`'ed parameter
-of the current function, and thus we can peek at that to know which function is making the call.
+The subgoals, created by `mkDecreasingProof`, are of the form `[data _recApp: rel arg param]`, where
+`param` is the `PackMutual`'ed parameter of the current function, and thus we can peek at that to
+know which function is making the call.
 The close coupling with how arguments are packed and termination goals look like is not great,
 but it works for now.
 -/