+theorem exp_sigma_p1: \forall n,a,p,f.
+pi_p n p (\lambda x.(exp a (f x))) = (exp a (sigma_p n p f)).
+intros.
+elim n
+ [reflexivity
+ |apply (bool_elim ? (p n1))
+ [intro.
+ rewrite > true_to_pi_p_Sn
+ [rewrite > true_to_sigma_p_Sn
+ [simplify.
+ rewrite > H.
+ rewrite > exp_plus_times.
+ reflexivity.
+ |assumption
+ ]
+ |assumption
+ ]
+ |intro.
+ rewrite > false_to_pi_p_Sn
+ [rewrite > false_to_sigma_p_Sn
+ [simplify.assumption
+ |assumption
+ ]
+ |assumption
+ ]
+ ]
+ ]
+qed.
+