simp [ih]
case cons
σ A R : Type
inst✝ : CommSemiring R
f : A → R
hd : A
tl : List A
ih : (List.map (fun x => C (f x)) tl).sum = C (List.map f tl).sum
⊢ (List.map (fun x => C (f x)) (hd :: tl)).sum = C (List.map f (hd :: tl)).sum
no goals