induction xs with
| nil => simp [filter]
| cons x xs ih =>
  simp only [filter]
  have : decide (¬x ∈ acc) = true := by simp [h x (Mem.head _)]
  rw [this]
  simp only
  rw [ih]
  . intros x hx
    apply h x (Mem.tail _ hx)
α : Type u_1
inst✝ : DecidableEq α
xs acc : List α
h : ∀ (x : α), x ∈ xs → ¬x ∈ acc
⊢ filter (fun a => decide ¬a ∈ acc) xs = xs
no goals