contradiction
case head
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
ys✝ : List (κ × ν)
k k' : κ
v : ν
ys : List (κ × ν)
h_term : length (matchKey ys k).snd < Nat.succ (length ys)
h_term' : length ys < Nat.succ (length ys)
hkeq : k' = k
h : ¬(k', v).fst = k
⊢ (k', v).fst ∈ map Prod.fst ys
no goals