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.
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.