apply all_in_map_fst_groupByKey_of_sublist this
case tail.a
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
xs✝ ys✝ xs ys : List (κ × ν)
k : κ
v : ν
hsubl : xs <+ ys
x : κ
htail : Mem x (map Prod.fst (groupByKey (matchKey xs k).snd))
this : (matchKey xs k).snd <+ (matchKey ys k).snd
hterm : length (matchKey ys k).snd < Nat.succ (length ys)
⊢ Mem x (map Prod.fst (groupByKey (matchKey ys k).snd))
case tail.a.a
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
xs✝ ys✝ xs ys : List (κ × ν)
k : κ
v : ν
hsubl : xs <+ ys
x : κ
htail : Mem x (map Prod.fst (groupByKey (matchKey xs k).snd))
this : (matchKey xs k).snd <+ (matchKey ys k).snd
hterm : length (matchKey ys k).snd < Nat.succ (length ys)
⊢ x ∈ map Prod.fst (groupByKey (matchKey xs k).snd)