rw [ih _ hk]
case cons.inl
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih :
  ∀ (acc : List κ),
    k ∈ acc → length (uniqueAux (map Prod.fst xs) acc) = length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc)
acc : List κ
hk : k ∈ acc
hin : x.fst ∈ acc
⊢ length (uniqueAux (map Prod.fst xs) acc) =
    length
      (uniqueAux
        (map Prod.fst
          (if x.fst = k then (x.snd :: (matchKey xs k).fst, (matchKey xs k).snd)
            else ((matchKey xs k).fst, (x.fst, x.snd) :: (matchKey xs k).snd)).snd)
        acc)
case cons.inl
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih :
  ∀ (acc : List κ),
    k ∈ acc → length (uniqueAux (map Prod.fst xs) acc) = length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc)
acc : List κ
hk : k ∈ acc
hin : x.fst ∈ acc
⊢ length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc) =
    length
      (uniqueAux
        (map Prod.fst
          (if x.fst = k then (x.snd :: (matchKey xs k).fst, (matchKey xs k).snd)
            else ((matchKey xs k).fst, (x.fst, x.snd) :: (matchKey xs k).snd)).snd)
        acc)