simp only [map, heq]
case cons.inl.a
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
heq : a.fst = x
⊢ x ∈ map Prod.fst (a :: as)
case cons.inl.a
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
heq : a.fst = x
⊢ x ∈ x :: map Prod.fst as