apply Sublist.cons _ _ _ ih
case cons.inr
κ : 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
hneq : ¬x'.fst = k
⊢ (matchKey xs' k).snd <+ (x'.fst, x'.snd) :: (matchKey ys' k).snd
no goals