{motive : Lean.Lsp.DocumentHighlightKind → Sort u} →
  (t : Lean.Lsp.DocumentHighlightKind) →
    motive Lean.Lsp.DocumentHighlightKind.text →
      motive Lean.Lsp.DocumentHighlightKind.read → motive Lean.Lsp.DocumentHighlightKind.write → motive t