induction xs generalizing acc with
| nil => simp [foldl, uniqueAux]
| cons x xs ih =>
  simp only [uniqueAux, foldl]
  cases acc with
  | nil =>
    simp only [incrCounts, map, List.not_mem_nil, ite_false]
    apply ih
  | cons a as =>
    simp only [incrCounts]
    cases Decidable.em (a.1 = x) with
    | inl htrue =>
      simp only [htrue, ite_true, incrCounts, map]
      rw [if_pos]
      . apply ih
      . exact List.Mem.head _
    | inr hfalse =>
      simp only [hfalse, ite_false, incrCounts, map]
      rw [ih]
      cases Decidable.em (x ∈ map Prod.fst as) with
      | inl hin =>
        have : x ∈ a.1 :: map Prod.fst as := List.Mem.tail _ hin
        simp only [this, ite_true, map, uniqueAux]
        apply congrArg
        apply congrArg
        apply congrArg
        exact map_fst_incrCounts_eq_map_fst x as hin
      | inr hout =>
        have : ¬ (x ∈ a.1 :: map Prod.fst as) := by
          intros hneg; cases hneg; repeat contradiction
        simp only [this, ite_false, map]
        rw [map_fst_incrCounts_eq_cons_fst _ _ hout]
        apply List.length_uniqueAux_congr_append_cons_acc _ _ _ _ []
α : Type u_1
inst✝ : DecidableEq α
xs : List α
acc : List (α × Nat)
⊢ length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
no goals