cases xs with
| nil => apply congrArg; simp [filter]
| cons x xs =>
  apply congrArg
  rw [this]
α : Type u_1
inst✝ : DecidableEq α
xs acc : List α
h : ∀ (x : α), x ∈ xs → ¬x ∈ acc
this : filter (fun a => decide ¬a ∈ acc) xs = xs
⊢ reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs) = reverse acc ++ unique xs
no goals