induction xs with
| nil => exact Nat.le.refl
| cons x xs ih =>
  simp only [matchKey]
  apply @Decidable.byCases (x.1=k) _
  . intros heq
    simp only [heq]
    rw [ite_true]
    simp only [Prod.snd]
    apply Nat.le_step
    exact ih
  . intros hneq
    simp only [hneq]
    rw [ite_false]
    simp only [Prod.fst]
    apply Nat.succ_le_succ
    exact ih
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
xs : List (κ × ν)
k : κ
⊢ length (matchKey xs k).snd ≤ length xs
no goals