∀ {textDocument : Lean.Lsp.VersionedTextDocumentIdentifier} {processing : Array Lean.Lsp.LeanFileProgressProcessingInfo}
  {textDocument_1 : Lean.Lsp.VersionedTextDocumentIdentifier}
  {processing_1 : Array Lean.Lsp.LeanFileProgressProcessingInfo},
  { textDocument := textDocument, processing := processing } =
      { textDocument := textDocument_1, processing := processing_1 } →
    textDocument = textDocument_1 ∧ processing = processing_1