simp only [split, length]
α : Type u_1
x y : α
xs : List α
ih : length (split xs).fst + length (split xs).snd = length xs
⊢ length (split (x :: y :: xs)).fst + length (split (x :: y :: xs)).snd = length (x :: y :: xs)
α : Type u_1
x y : α
xs : List α
ih : length (split xs).fst + length (split xs).snd = length xs
⊢ length (split xs).fst + 1 + (length (split xs).snd + 1) = length xs + 1 + 1