cases hneg with
| head => exact absurd rfl hneq
| tail _ h => exact h
case cons.inr
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (matchKey kvs k).snd → False
hneq : ¬kv.fst = k
hneg : k ∈ kv.fst :: map Prod.fst (matchKey kvs k).snd
⊢ k ∈ map Prod.fst (matchKey kvs k).snd
no goals