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