+theorem eq_iter_p_gen_pred:
+\forall A:Type.
+\forall baseA: A.
+\forall plusA: A \to A \to A.
+\forall n,p,g.
+p O = true \to
+(symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a baseA) = a) \to
+iter_p_gen (S n) (\lambda i.p (pred i)) A (\lambda i.g(pred i)) baseA plusA =
+plusA (iter_p_gen n p A g baseA plusA) (g O).
+intros.
+elim n
+ [rewrite > true_to_iter_p_gen_Sn
+ [simplify.apply H1
+ |assumption
+ ]
+ |apply (bool_elim ? (p n1));intro
+ [rewrite > true_to_iter_p_gen_Sn
+ [rewrite > true_to_iter_p_gen_Sn in ⊢ (? ? ? %)
+ [rewrite > H2 in ⊢ (? ? ? %).
+ apply eq_f.assumption
+ |assumption
+ ]
+ |assumption
+ ]
+ |rewrite > false_to_iter_p_gen_Sn
+ [rewrite > false_to_iter_p_gen_Sn in ⊢ (? ? ? %);assumption
+ |assumption
+ ]
+ ]
+ ]
+qed.
+