have : filter (fun a => decide ¬a ∈ acc) xs = xs := by
  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
⊢ uniqueAux xs acc = reverse acc ++ unique xs
α : Type u_1
inst✝ : DecidableEq α
xs acc : List α
h : ∀ (x : α), x ∈ xs → ¬x ∈ acc
this : filter (fun a => decide ¬a ∈ acc) xs = xs
⊢ uniqueAux xs acc = reverse acc ++ unique xs