{P : Sort u} →
  {toTextDocumentPositionParams toTextDocumentPositionParams' : Lean.Lsp.TextDocumentPositionParams} →
    { toTextDocumentPositionParams := toTextDocumentPositionParams } =
        { toTextDocumentPositionParams := toTextDocumentPositionParams' } →
      (toTextDocumentPositionParams = toTextDocumentPositionParams' → P) → P