∀ {α : Type u_1} {β : Type u_2} (motive : List α → List β → Sort u_3) (bs : List β) (h_1 : (bs : List β) → motive [] bs)
  (h_2 : (a : α) → (as : List α) → (bs : List β) → motive (a :: as) bs),
  (match [], bs with
    | [], bs => h_1 bs
    | a :: as, bs => h_2 a as bs) =
    h_1 bs