cases h with
| head => apply Mem.head
| tail _ htail =>
  apply Mem.tail
  apply ih
  apply all_in_map_fst_groupByKey_of_sublist (matchKey_snd_sublist k₀ kvs)
  assumption
case cons.mk
κ : Type u_1
ν : Type u_2
k : κ
inst✝ : DecidableEq κ
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (groupByKey kvs) → k ∈ map Prod.fst kvs
k₀ : κ
v₀ : ν
h : k ∈ k₀ :: map Prod.fst (groupByKey (matchKey kvs k₀).snd)
⊢ k ∈ k₀ :: map Prod.fst kvs
no goals