{α : Type} →
  {P : Sort u} →
    {β : Type} →
      {selector : Std.Internal.IO.Async.Selector β} →
        {cont : β → Std.Internal.IO.Async.Async α} →
          {β' : Type} →
            {selector' : Std.Internal.IO.Async.Selector β'} →
              {cont' : β' → Std.Internal.IO.Async.Async α} →
                { β := β, selector := selector, cont := cont } = { β := β', selector := selector', cont := cont' } →
                  (β = β' → selector ≍ selector' → cont ≍ cont' → P) → P