apply List.length_uniqueAux (acc := [k])
case h
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
k : κ
v : ν
xs : List (κ × ν)
hterm : length (matchKey xs k).snd < Nat.succ (length xs)
ih : length (groupByKey (matchKey xs k).snd) = length (unique (map Prod.fst (matchKey xs k).snd))
⊢ length (uniqueAux (map Prod.fst (matchKey xs k).snd) [k]) = length (unique (map Prod.fst (matchKey xs k).snd)) + 1
case h.h
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
k : κ
v : ν
xs : List (κ × ν)
hterm : length (matchKey xs k).snd < Nat.succ (length xs)
ih : length (groupByKey (matchKey xs k).snd) = length (unique (map Prod.fst (matchKey xs k).snd))
⊢ ∀ (x : κ), x ∈ map Prod.fst (matchKey xs k).snd → ¬x ∈ [k]