simp only [hneq, ite_false] at hneg
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
hneg :
  k ∈
    map Prod.fst
      (if kv.fst = k then (kv.snd :: (matchKey kvs k).fst, (matchKey kvs k).snd)
        else ((matchKey kvs k).fst, (kv.fst, kv.snd) :: (matchKey kvs k).snd)).snd
hneq : ¬kv.fst = k
⊢ k ∈ map Prod.fst (matchKey kvs k).snd
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 ∈ map Prod.fst ((kv.fst, kv.snd) :: (matchKey kvs k).snd)
⊢ k ∈ map Prod.fst (matchKey kvs k).snd