apply congrArg
case nil
α : Type u_1
inst✝ : DecidableEq α
acc : List α
h : ∀ (x : α), x ∈ [] → ¬x ∈ acc
this : filter (fun a => decide ¬a ∈ acc) [] = []
⊢ reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) []) = reverse acc ++ unique []
case nil.h
α : Type u_1
inst✝ : DecidableEq α
acc : List α
h : ∀ (x : α), x ∈ [] → ¬x ∈ acc
this : filter (fun a => decide ¬a ∈ acc) [] = []
⊢ unique (filter (fun x => decide ¬x ∈ acc) []) = unique []