rw [reverse_singleton, singleton_append, filter_filter]
case inr.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
⊢ x :: uniqueAux (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs) [] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
case inr.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
⊢ x :: uniqueAux (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs) [] =
    x :: unique (filter (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) xs)