exact ih in_tail
case cons.inr.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'
in_tail : a ∈ t
⊢ List.length (List.remove a t) < List.length t
no goals