∀ {M : Type u_1} (motive : List M → List M → Prop) (x x_1 : List M),
  (∀ (ys : List M), motive [] ys) →
    (∀ (xs : List M), motive xs []) →
      (∀ (x : M) (xs : List M) (y : M) (ys : List M), motive (x :: xs) (y :: ys)) → motive x x_1