have hterm : length (matchKey xs k).snd < Nat.succ (length xs) :=
  Nat.lt_of_succ_le $ Nat.succ_le_succ $ matchKey_snd_length xs k
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
k : κ
v : ν
xs : List (κ × ν)
⊢ length (groupByKey ((k, v) :: xs)) = length (unique (map Prod.fst ((k, v) :: xs)))
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
k : κ
v : ν
xs : List (κ × ν)
hterm : length (matchKey xs k).snd < Nat.succ (length xs)
⊢ length (groupByKey ((k, v) :: xs)) = length (unique (map Prod.fst ((k, v) :: xs)))