simp only [matchKey, length, ite_true]
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
v : ν
xs : List (κ × ν)
⊢ 1 + length (groupByKey (matchKey ((k, v) :: xs) k).snd) = 1 + length (groupByKey (matchKey xs k).snd)
no goals