-theorem pi_p_SO: \forall n,p.
-pi_p n p (\lambda i.S O) = S O.
-intros.elim n
- [reflexivity
- |simplify.elim (p n1)
- [simplify.rewrite < plus_n_O.assumption
- |simplify.assumption
- ]
- ]
-qed.
-
-theorem exp_pi_p: \forall n,m,p,f.
-pi_p n p (\lambda x.exp (f x) m) = exp (pi_p n p f) m.
-intros.
-elim m
- [simplify.apply pi_p_SO
- |simplify.
- rewrite > times_pi_p.
- rewrite < H.
- reflexivity
- ]
-qed.