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