rw [Nat.add_assoc, Nat.add_comm 1, ←Nat.add_assoc]
case cons.isTrue
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).fst + length (matchKey xs k).snd = length xs
htrue : x.fst = k
⊢ length (matchKey xs k).fst + 1 + length (matchKey xs k).snd = length xs + 1
case cons.isTrue
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).fst + length (matchKey xs k).snd = length xs
htrue : x.fst = k
⊢ length (matchKey xs k).fst + length (matchKey xs k).snd + 1 = length xs + 1