{motive : Lean.Lsp.LeanFileProgressParams → Sort u} →
  ((textDocument : Lean.Lsp.VersionedTextDocumentIdentifier) →
      (processing : Array Lean.Lsp.LeanFileProgressProcessingInfo) →
        motive { textDocument := textDocument, processing := processing }) →
    (t : Lean.Lsp.LeanFileProgressParams) → motive t