{P : Sort u} →
  {location : Lean.Lsp.Location} →
    {message : String} →
      {location' : Lean.Lsp.Location} →
        {message' : String} →
          { location := location, message := message } = { location := location', message := message' } →
            (location = location' → message = message' → P) → P