∀ {α : Type u_1} (motive : (x x_1 x_2 x_3 : List α) → x ++ x_2 = x_1 ++ x_3 → x.length = x_1.length → Prop)
  (x x_1 x_2 x_3 : List α) (x_4 : x ++ x_2 = x_1 ++ x_3) (x_5 : x.length = x_1.length),
  (∀ (x x_6 : List α) (h : [] ++ x = [] ++ x_6) (x_7 : [].length = [].length), motive [] [] x x_6 h x_7) →
    (∀ (head : α) (tail : List α) (head_1 : α) (tail_1 x x_6 : List α) (h : head :: tail ++ x = head_1 :: tail_1 ++ x_6)
        (hl : (head :: tail).length = (head_1 :: tail_1).length), motive (head :: tail) (head_1 :: tail_1) x x_6 h hl) →
      motive x x_1 x_2 x_3 x_4 x_5