{α β : Type} →
  {motive : Std.Internal.Async.IO.AsyncWrite α β → Sort u} →
    ((write : α → β → Std.Internal.IO.Async.Async Unit) →
        (writeAll : α → Array β → Std.Internal.IO.Async.Async Unit) →
          (flush : α → Std.Internal.IO.Async.Async Unit) →
            motive { write := write, writeAll := writeAll, flush := flush }) →
      (t : Std.Internal.Async.IO.AsyncWrite α β) → motive t