rw [ite_true]
case cons.h1
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
heq : x.fst = k
⊢ length
      (if True then (x.snd :: (matchKey xs k).fst, (matchKey xs k).snd)
        else ((matchKey xs k).fst, (k, x.snd) :: (matchKey xs k).snd)).snd ≤
    length (x :: xs)
case cons.h1
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
heq : x.fst = k
⊢ length (x.snd :: (matchKey xs k).fst, (matchKey xs k).snd).snd ≤ length (x :: xs)