{α : Type} →
  (motive : List (Task α) → Sort u_1) →
    (x : List (Task α)) →
      (x = [] → motive []) →
        ((task : Task α) → (rest : List (Task α)) → x = task :: rest → motive (task :: rest)) → motive x