assumption
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
kvs : List (κ × ν)
a✝ :
  ∀ (y : List (κ × ν)),
    (invImage (fun a => length a) instWellFoundedRelation).1 y kvs → map Prod.fst (groupByKey y) <+ map Prod.fst y
k : κ
v : ν
xs : List (κ × ν)
x✝ :
  ∀ (y : List (κ × ν)),
    (invImage (fun a => length a) instWellFoundedRelation).1 y ((k, v) :: xs) →
      map Prod.fst (groupByKey y) <+ 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