induction xs with
| nil => intros; simp [uniqueAux]
| cons x xs ih =>
  intros acc hk
  simp only [length, uniqueAux]
  cases Decidable.em (x.fst ∈ acc) with
  | inl hin =>
    simp only [hin, ite_true, matchKey]
    rw [ih _ hk]
    cases Decidable.em (x.1 = k) with
    | inl heq => simp only [heq, ite_true]
    | inr hneq => simp only [hneq, ite_false, map, uniqueAux, hin, ite_true]
  | inr hout =>
    simp only [hout, ite_false, matchKey]
    cases Decidable.em (x.1 = k) with
    | inl heq =>
      apply absurd hk
      rw [heq] at hout
      exact hout
    | inr hneq =>
      rw [ih _ (List.Mem.tail _ hk)]
      simp only [hneq, ite_false, uniqueAux, hout]
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
xs : List (κ × ν)
k : κ
⊢ ∀ (acc : List κ),
    k ∈ acc → length (uniqueAux (map Prod.fst xs) acc) = length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc)
no goals