simp only [matchKey]
case cons2
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
⊢ (matchKey (x' :: xs') k).snd <+ (matchKey (x' :: ys') k).snd
case cons2
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
xs' ys' : List (κ × ν)
x' : κ × ν
h' : xs' <+ ys'
ih : (matchKey xs' k).snd <+ (matchKey ys' k).snd
⊢ (if x'.fst = k then (x'.snd :: (matchKey xs' k).fst, (matchKey xs' k).snd)
      else ((matchKey xs' k).fst, (x'.fst, x'.snd) :: (matchKey xs' k).snd)).snd <+
    (if x'.fst = k then (x'.snd :: (matchKey ys' k).fst, (matchKey ys' k).snd)
      else ((matchKey ys' k).fst, (x'.fst, x'.snd) :: (matchKey ys' k).snd)).snd