assumption
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
xs✝ : List (κ × ν)
a✝ :
  ∀ (y : List (κ × ν)),
    (invImage (fun a => length a) instWellFoundedRelation).1 y xs✝ →
      length (groupByKey y) = length (unique (map Prod.fst y))
k : κ
v : ν
xs : List (κ × ν)
x✝ :
  ∀ (y : List (κ × ν)),
    (invImage (fun a => length a) instWellFoundedRelation).1 y ((k, v) :: xs) →
      length (groupByKey y) = length (unique (map Prod.fst y))
hterm : length (matchKey xs k).snd < Nat.succ (length xs)
⊢ (invImage (fun a => length a) instWellFoundedRelation).1 (matchKey xs k).snd ((k, v) :: xs)
no goals