|reflexivity]]
|reflexivity]
|reflexivity]]
+qed.
+
+theorem exp_S_sigma_p:\forall a,n.
+exp (S a) n = sigma_p (S n) (\lambda k.true) (\lambda k.(bc n k)*(exp a (n-k))).
+intros.
+rewrite > plus_n_SO.
+rewrite > exp_plus_sigma_p.
+apply eq_sigma_p;intros
+ [reflexivity
+ |rewrite < exp_SO_n.
+ rewrite < times_n_SO.
+ reflexivity
+ ]
qed.
\ No newline at end of file