rw [this]
case cons.h
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x : α
xs : List α
h : ∀ (x_1 : α), x_1 ∈ x :: xs → ¬x_1 ∈ acc
this : filter (fun a => decide ¬a ∈ acc) (x :: xs) = x :: xs
⊢ unique (filter (fun x => decide ¬x ∈ acc) (x :: xs)) = unique (x :: xs)
no goals