cases Decidable.em (x ∈ acc) with
| inl hin =>
  simp only [hin, ite_true, not_true_eq_false, decide_False]
  rw [ih₁]
| inr hout =>
  simp only [hout, ite_false, not_false_eq_true, decide_True]
  simp only [reverse_singleton, singleton_append, unique,
             uniqueAux, List.not_mem_nil, ite_false]
  rw [ih₂]
  simp only [reverse_cons, append_assoc, singleton_append]
  apply congrArg
  simp only [unique]
  rw [ih₃]
  rw [reverse_singleton, singleton_append, filter_filter]
  have : (λ x_1 => decide (
          (decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)
         ) = (λ x_1 => decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])) := by
    apply funext
    intro x_1
    simp only [decide_not, Bool.not_eq_true']
    cases Decidable.em (x_1 ∈ acc) with
    | inl hmem =>
      simp only [hmem, decide_True, not_true_eq_false, false_and]
    | inr hnmem =>
      simp only [hnmem, decide_False, not_false_eq_true, true_and,
                 decide_not]
      cases Decidable.em (x_1 ∈ [x]) with
      | inl hmem' => simp only [hmem', decide_True, decide_False, not]
      | inr hnmem' => simp only [hnmem', decide_True, decide_False, not]
  rw [this, ←unique]
  apply congrArg
  apply congrArg
  have h_mem_iff := mem_cons_iff_mem_singleton_or_tail x acc
  have h_mem_iff_neg := (λ x => Iff.not_iff_not_of_iff $ h_mem_iff x)
  apply congr _ rfl
  apply congr rfl
  apply funext
  intros a
  apply Decidable.prop_eq_of_decide_eq
  rw [h_mem_iff_neg, not_or_distrib, And.comm]
α : 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))
⊢ (if x ∈ acc then uniqueAux xs acc else uniqueAux xs (x :: acc)) =
    reverse acc ++
      unique
        (match decide ¬x ∈ acc with
        | true => x :: filter (fun x => decide ¬x ∈ acc) xs
        | false => filter (fun x => decide ¬x ∈ acc) xs)
no goals