intros xs k
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
⊢ ∀ (xs : List (κ × ν)) (k : κ), length (matchKey xs k).snd ≤ length xs
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
xs : List (κ × ν)
k : κ
⊢ length (matchKey xs k).snd ≤ length xs