apply Nat.le_step
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.inl.h
α : 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) ≤ List.length t