∀ {α : Type u_1} (motive : List α → Sort u_2) (b : α) (l : List α) (h_1 : Unit → motive [])
  (h_2 : (b : α) → (l : List α) → motive (b :: l)),
  (match b :: l with
    | [] => h_1 ()
    | b :: l => h_2 b l) =
    h_2 b l