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