apply Mem.head
case cons.mk.head
κ : Type u_1
ν : Type u_2
k : κ
inst✝ : DecidableEq κ
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (groupByKey kvs) → k ∈ map Prod.fst kvs
v₀ : ν
⊢ k ∈ k :: map Prod.fst kvs
no goals