qed.
theorem sigma_p_plus_1: \forall n:nat. \forall f,g:nat \to nat.
-sigma_p n (\lambda b:nat. true) (\lambda a:nat.(f a) + (g a)) =
-sigma_p n (\lambda b:nat. true) f + sigma_p n (\lambda b:nat. true) g.
+\forall p.
+sigma_p n p (\lambda a:nat.(f a) + (g a)) =
+sigma_p n p f + sigma_p n p g.
intros.
elim n
[ simplify.
reflexivity
-| rewrite > true_to_sigma_p_Sn
- [ rewrite > (true_to_sigma_p_Sn n1 (\lambda c:nat.true) f)
- [ rewrite > (true_to_sigma_p_Sn n1 (\lambda c:nat.true) g)
- [ rewrite > assoc_plus in \vdash (? ? ? %).
- rewrite < assoc_plus in \vdash (? ? ? (? ? %)).
- rewrite < sym_plus in \vdash (? ? ? (? ? (? % ?))).
- rewrite > assoc_plus in \vdash (? ? ? (? ? %)).
- rewrite < assoc_plus in \vdash (? ? ? %).
- apply eq_f.
- assumption
- | reflexivity
- ]
- | reflexivity
- ]
- | reflexivity
- ]
-]
+| apply (bool_elim ? (p n1)); intro;
+ [ rewrite > true_to_sigma_p_Sn
+ [ rewrite > (true_to_sigma_p_Sn n1 p f)
+ [ rewrite > (true_to_sigma_p_Sn n1 p g)
+ [ rewrite > assoc_plus in \vdash (? ? ? %).
+ rewrite < assoc_plus in \vdash (? ? ? (? ? %)).
+ rewrite < sym_plus in \vdash (? ? ? (? ? (? % ?))).
+ rewrite > assoc_plus in \vdash (? ? ? (? ? %)).
+ rewrite < assoc_plus in \vdash (? ? ? %).
+ apply eq_f.
+ assumption]]]
+ assumption
+ | rewrite > false_to_sigma_p_Sn
+ [ rewrite > (false_to_sigma_p_Sn n1 p f)
+ [ rewrite > (false_to_sigma_p_Sn n1 p g)
+ [assumption]]]
+ assumption
+]]
qed.
-
theorem eq_sigma_p_sigma_p_times1 : \forall n,m:nat.\forall f:nat \to nat.
sigma_p (n*m) (\lambda x:nat.true) f =
sigma_p m (\lambda x:nat.true)