{ε : 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} →
            (t : Except ε (IO.AsyncList ε α)) →
              ((t : IO.AsyncList ε α) → t.below → motive_1 t) →
                ((t : Lean.Server.ServerTask (Except ε (IO.AsyncList ε α))) → IO.AsyncList.below_1 t → motive_2 t) →
                  ((t : Task (Except ε (IO.AsyncList ε α))) → IO.AsyncList.below_2 t → motive_3 t) →
                    ((t : Except ε (IO.AsyncList ε α)) → IO.AsyncList.below_3 t → motive_4 t) → motive_4 t