exact ih
case cons.h2.a
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
hneq : ¬x.fst = k
⊢ length (matchKey xs k).snd ≤ length xs
no goals