intro xs x hnmem
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ (xs : List α) (x : α), ¬x ∈ xs → removeAllEq xs [x] = xs
α : Type u_1
inst✝ : DecidableEq α
xs : List α
x : α
hnmem : ¬x ∈ xs
⊢ removeAllEq xs [x] = xs