{P : Sort u} →
  {textDocument : Lean.Lsp.VersionedTextDocumentIdentifier} →
    {edits : Lean.Lsp.TextEditBatch} →
      {textDocument' : Lean.Lsp.VersionedTextDocumentIdentifier} →
        {edits' : Lean.Lsp.TextEditBatch} →
          { textDocument := textDocument, edits := edits } = { textDocument := textDocument', edits := edits' } →
            (textDocument = textDocument' → edits = edits' → P) → P