induction xs with
| nil => rfl
| cons x xs ih =>
  simp only [matchKey]
  cases inst x.1 k with
  | isFalse hfalse =>
    simp only [hfalse, ite_false, ih, filter]
    exact rfl
  | isTrue htrue =>
    simp [htrue, ite_true, filter, ih, map]
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
xs : List (κ × ν)
k : κ
⊢ (matchKey xs k).fst = map Prod.snd (filter (fun x => decide (x.fst = k)) xs)
no goals