apply h x (Mem.tail _ hx)
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 : α), x ∈ x✝ :: xs → ¬x ∈ acc
this : (decide ¬x✝ ∈ acc) = true
x : α
hx : x ∈ xs
⊢ ¬x ∈ acc
no goals