simp only [removeAllEq, filter, notElem, elem, hneq, not]
α : Type u_1
inst✝ : DecidableEq α
x y : α
xs : List α
hneq : x ≠ y
⊢ removeAllEq (x :: xs) [y] = x :: removeAllEq xs [y]
α : Type u_1
inst✝ : DecidableEq α
x y : α
xs : List α
hneq : x ≠ y
⊢ (match decide ¬x ∈ [y] with
    | true => x :: filter (fun x => decide ¬x ∈ [y]) xs
    | false => filter (fun x => decide ¬x ∈ [y]) xs) =
    x :: filter (fun x => decide ¬x ∈ [y]) xs