{α : Type u_1} →
  {motive : List α → Sort u_2} →
    motive [] →
      ((a : α) → motive [a]) →
        ((a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b]))) → (l : List α) → motive l