Sum over fin with index offset on terms

Stream: Is there code for X?

[Aras Yilmaz]

I need to prove the following goal:

T : Type u_1
c : List Bool
tl : List T
f : T → SLang Bool
⊢ (∑' (a : List Bool), if c = a then mapM f tl a else 0) = mapM f tl c

Can anyone help me?

[Notification Bot]

Aras Yilmaz has marked this topic as unresolved.

[Kevin Buzzard]

Can you post a #mwe ?