{t m : Type → Type} →
  {motive : Std.Internal.IO.Async.MonadAsync t m → Sort u} →
    ((async : {α : Type} → m α → optParam Task.Priority Task.Priority.default → m (t α)) → motive { async := async }) →
      (t : Std.Internal.IO.Async.MonadAsync t m) → motive t