rw [removeAllEq_singleton_hd_neq]
case cons
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ removeAllEq (x' :: xs) [x] = x' :: xs
case cons
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' :: removeAllEq xs [x] = x' :: xs

case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' ≠ x