{α : Type u_1} →
  (motive : List α → List α → Sort u_2) →
    (x x_1 : List α) →
      ((x : List α) → motive [] x) →
        ((x : List α) → (x = [] → False) → motive x []) →
          ((a : α) → (as : List α) → (b : α) → (bs : List α) → motive (a :: as) (b :: bs)) → motive x x_1