∀F,p:Top.  (weighted-sum([p];F) ~ 0 + ((F 0) * p))
{ (UnivCD THENA Auto) }
1. F : Top@i
2. p : Top@i
⊢ weighted-sum([p];F) ~ 0 + ((F 0) * p)