{motive : Lean.Server.Logging.MessageMethod → Sort u} →
  (t : Lean.Server.Logging.MessageMethod) →
    t.ctorIdx = 0 → ((method : String) → motive (Lean.Server.Logging.MessageMethod.request method)) → motive t