{motive : Lean.Server.FileWorker.LakeSetupFileOutput → Sort u} →
  ((spawnArgs : IO.Process.SpawnArgs) →
      (exitCode : UInt32) →
        (stdout stderr : String) →
          motive { spawnArgs := spawnArgs, exitCode := exitCode, stdout := stdout, stderr := stderr }) →
    (t : Lean.Server.FileWorker.LakeSetupFileOutput) → motive t