{α : Type} →
  {motive : Lean.Server.ServerRequestResponse α → Sort u} →
    (ctorIdx : ℕ) →
      (t : Lean.Server.ServerRequestResponse α) →
        ctorIdx = t.ctorIdx → Lean.Server.ServerRequestResponse.ctorElimType ctorIdx → motive t