split
case cons
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : List.length (List.remove a t) ≤ List.length t
⊢ List.length (if a = h' then List.remove a t else h' :: List.remove a t) ≤ Nat.succ (List.length t)
case cons.inl
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : List.length (List.remove a t) ≤ List.length t
h✝ : a = h'
⊢ List.length (List.remove a t) ≤ Nat.succ (List.length t)

case cons.inr
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : List.length (List.remove a t) ≤ List.length t
h✝ : ¬a = h'
⊢ List.length (h' :: List.remove a t) ≤ Nat.succ (List.length t)