cases hx with
| head => constructor
| tail _ htail =>
  apply Mem.tail
  have : (matchKey xs k).snd <+ (matchKey ys k).snd :=
    matchKey_snd_sublist_of_sublist _ _ _ hsubl
  have hterm := matchKey_length_lt k ys
  apply all_in_map_fst_groupByKey_of_sublist this
  assumption
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
xs✝ ys✝ xs ys : List (κ × ν)
k : κ
v : ν
hsubl : xs <+ ys
x : κ
hx : x ∈ k :: map Prod.fst (groupByKey (matchKey xs k).snd)
⊢ x ∈ k :: map Prod.fst (groupByKey (matchKey ys k).snd)
no goals