apply congrArg (λ x => x + (1 + 1))
α : Type u_1
x y : α
xs : List α
ih : length (split xs).fst + length (split xs).snd = length xs
⊢ length (split xs).fst + length (split xs).snd + (1 + 1) = length xs + (1 + 1)
α : Type u_1
x y : α
xs : List α
ih : length (split xs).fst + length (split xs).snd = length xs
⊢ length (split xs).fst + length (split xs).snd = length xs