simp [List.remove]
case cons
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : List.length (List.remove a t) ≤ List.length t
⊢ List.length (List.remove a (h' :: t)) ≤ List.length (h' :: t)
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)