]
qed.
-(*distributive propery for sigma_p_gen*)
+(*distributive property for sigma_p_gen*)
theorem distributive_times_plus_sigma_p_generic: \forall A:Type.
\forall plusA: A \to A \to A. \forall basePlusA: A.
\forall timesA: A \to A \to A.
\to
((timesA k (sigma_p_gen n p A g basePlusA plusA)) =
- (sigma_p_gen n p A (\lambda i:nat.(timesA (g i) k)) basePlusA plusA)).
+ (sigma_p_gen n p A (\lambda i:nat.(timesA k (g i))) basePlusA plusA)).
intros.
elim n
[ simplify.