{motive : Lean.Lsp.Command → Sort u} →
  (t : Lean.Lsp.Command) →
    ((title command : String) →
        (arguments? : Option (Array Lean.Json)) →
          motive { title := title, command := command, arguments? := arguments? }) →
      motive t