{α : Type} →
  {motive : Std.Internal.IO.Async.Selectable α → Sort u} →
    (t : Std.Internal.IO.Async.Selectable α) →
      ({β : Type} →
          (selector : Std.Internal.IO.Async.Selector β) →
            (cont : β → Std.Internal.IO.Async.Async α) → motive { β := β, selector := selector, cont := cont }) →
        motive t