X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fiteration2.ma;h=211df69d0fa0d9941a9dcf14bebca51e1812ffda;hb=10f29fdd78ee089a9a94446207b543d33d6c851c;hp=6dbbfd572a2ac824de1d69bff781d06eb18009cc;hpb=9edc9828ff3c3d074ccc5547a53eadf092c186d8;p=helm.git

diff --git a/helm/software/matita/library/nat/iteration2.ma b/helm/software/matita/library/nat/iteration2.ma
index 6dbbfd572..211df69d0 100644
--- a/helm/software/matita/library/nat/iteration2.ma
+++ b/helm/software/matita/library/nat/iteration2.ma
@@ -629,32 +629,33 @@ elim n
 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)