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