{ε : Type u} →
  {α : Type v} →
    {motive_1 : IO.AsyncList ε α → Sort u_1} →
      {motive_2 : Lean.Server.ServerTask (Except ε (IO.AsyncList ε α)) → Sort u_1} →
        {motive_3 : Task (Except ε (IO.AsyncList ε α)) → Sort u_1} →
          {motive_4 : Except ε (IO.AsyncList ε α) → Sort u_1} →
            ((hd : α) → (tl : IO.AsyncList ε α) → motive_1 tl → motive_1 (IO.AsyncList.cons hd tl)) →
              ((tl : Lean.Server.ServerTask (Except ε (IO.AsyncList ε α))) →
                  motive_2 tl → motive_1 (IO.AsyncList.delayed tl)) →
                motive_1 IO.AsyncList.nil →
                  ((task : Task (Except ε (IO.AsyncList ε α))) → motive_3 task → motive_2 { task := task }) →
                    ((get : Except ε (IO.AsyncList ε α)) → motive_4 get → motive_3 { get := get }) →
                      ((a : ε) → motive_4 (Except.error a)) →
                        ((a : IO.AsyncList ε α) → motive_1 a → motive_4 (Except.ok a)) →
                          (t : IO.AsyncList ε α) → motive_1 t