simp only [split, length]
α : Type u_1
x₁ x₂ x x' : α
xs : List α
ih : length (x :: x' :: xs) ≤ 1 ∨ length (split (x :: x' :: xs)).fst < length (x :: x' :: xs)
⊢ length (x₁ :: x₂ :: x :: x' :: xs) ≤ 1 ∨
    length (split (x₁ :: x₂ :: x :: x' :: xs)).fst < length (x₁ :: x₂ :: x :: x' :: xs)
α : Type u_1
x₁ x₂ x x' : α
xs : List α
ih : length (x :: x' :: xs) ≤ 1 ∨ length (split (x :: x' :: xs)).fst < length (x :: x' :: xs)
⊢ length xs + 1 + 1 + 1 + 1 ≤ 1 ∨ length (split xs).fst + 1 + 1 < length xs + 1 + 1 + 1 + 1