{α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) →
      (Unit → motive []) →
        ((head : α) → motive [head]) → ((a : α) → (as : List α) → (as = [] → False) → motive (a :: as)) → motive x