induction kvs with
| nil => cases hneg
| cons kv kvs ih =>
  apply ih
  simp only [matchKey] at hneg
  cases Decidable.em (kv.fst = k) with
  | inl heq =>
    simp only [heq, ite_true] at hneg
    assumption
  | inr hneq =>
    simp only [hneq, ite_false] at hneg
    simp only [map] at hneg
    cases hneg with
    | head => exact absurd rfl hneq
    | tail _ h => exact h
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kvs : List (κ × ν)
hneg : k ∈ map Prod.fst (matchKey kvs k).snd
⊢ False
no goals