simp only [filter]
case cons
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → ¬x ∈ acc) → filter (fun a => decide ¬a ∈ acc) xs = xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → ¬x_1 ∈ acc
⊢ filter (fun a => decide ¬a ∈ acc) (x :: xs) = x :: xs
case cons
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → ¬x ∈ acc) → filter (fun a => decide ¬a ∈ acc) xs = xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → ¬x_1 ∈ acc
⊢ (match decide ¬x ∈ acc with
    | true => x :: filter (fun a => decide ¬a ∈ acc) xs
    | false => filter (fun a => decide ¬a ∈ acc) xs) =
    x :: xs