Improve comments

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.
 -/