simp [h x (Mem.head _)]
α : 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
⊢ (decide ¬x ∈ acc) = true
no goals