induction h with
| nil => constructor
| cons xs' ys' x' h' ih =>
  simp only [matchKey]
  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
| cons2 xs' ys' x' h' ih =>
  simp only [matchKey]
  cases Decidable.em (x'.fst = k) with
  | inl heq => simp only [heq, ite_true]; assumption
  | inr hneq =>
    simp only [hneq, ite_false]
    apply Sublist.cons2 _ _ _ ih
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
xs ys : List (κ × ν)
h : xs <+ ys
⊢ (matchKey xs k).snd <+ (matchKey ys k).snd
no goals