cases ih with
| inl _ => contradiction
| inr h => apply h
case h.a.a
α : Type u_1
x₁ x₂ x x' : α
xs : List α
ih : length xs + 1 + 1 ≤ 1 ∨ length (split xs).fst + 1 < length xs + 1 + 1
⊢ length (split xs).fst + 1 < length xs + 2
no goals