apply ih
case cons
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (matchKey kvs k).snd → False
hneg : k ∈ map Prod.fst (matchKey (kv :: kvs) k).snd
⊢ False
case cons
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (matchKey kvs k).snd → False
hneg : k ∈ map Prod.fst (matchKey (kv :: kvs) k).snd
⊢ k ∈ map Prod.fst (matchKey kvs k).snd