{motive : Lean.JsonRpc.Message → Sort u} →
  (t : Lean.JsonRpc.Message) →
    ((id : Lean.JsonRpc.RequestID) →
        (method : String) →
          (params? : Option Lean.Json.Structured) → motive (Lean.JsonRpc.Message.request id method params?)) →
      ((method : String) →
          (params? : Option Lean.Json.Structured) → motive (Lean.JsonRpc.Message.notification method params?)) →
        ((id : Lean.JsonRpc.RequestID) → (result : Lean.Json) → motive (Lean.JsonRpc.Message.response id result)) →
          ((id : Lean.JsonRpc.RequestID) →
              (code : Lean.JsonRpc.ErrorCode) →
                (message : String) →
                  (data? : Option Lean.Json) → motive (Lean.JsonRpc.Message.responseError id code message data?)) →
            motive t