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