intro hneg
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kvs : List (κ × ν)
⊢ ¬k ∈ map Prod.fst (matchKey kvs k).snd
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kvs : List (κ × ν)
hneg : k ∈ map Prod.fst (matchKey kvs k).snd
⊢ False