{motive : Lean.Server.Overview.NotificationOverview✝ → Sort u} →
  (t : Lean.Server.Overview.NotificationOverview✝) →
    ((method : String) →
        (direction : Lean.JsonRpc.MessageDirection) →
          (kinds : Array Lean.Server.Overview.ProtocolExtensionKind✝) →
            (parameterType : Type) →
              (description : String) →
                motive
                  { method := method, direction := direction, kinds := kinds, parameterType := parameterType,
                    description := description }) →
      motive t