apply Nat.lt_succ_of_le
case cons.inl
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: t
h✝ : a = h'
⊢ List.length (List.remove a t) < Nat.succ (List.length t)
case cons.inl.a
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: t
h✝ : a = h'
⊢ List.length (List.remove a t) ≤ List.length t