cases Decidable.em (x'.fst = k) with
| inl heq => simp only [heq, ite_true]; apply ih
| inr hneq => simp only [hneq, ite_false]; apply Sublist.cons _ _ _ ih
case cons
κ : 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 xs' k).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
no goals