exact rfl
case cons.isFalse
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : (matchKey xs k).fst = map Prod.snd (filter (fun x => decide (x.fst = k)) xs)
hfalse : ¬x.fst = k
⊢ map Prod.snd (filter (fun x => decide (x.fst = k)) xs) =
    map Prod.snd
      (match decide False with
      | true => x :: filter (fun x => decide (x.fst = k)) xs
      | false => filter (fun x => decide (x.fst = k)) xs)
no goals