X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fpi_p.ma;h=0c5e0d7014bda9cfcc98fb061738499b726d5211;hb=aa5f71baeba0299c0d29be01798f7a1ad13656f9;hp=93f127372410610e5147fe02c5bf3fa59a08b2c7;hpb=c445ba5534cccde19016c92660ab52777af221c0;p=helm.git

diff --git a/helm/software/matita/library/nat/pi_p.ma b/helm/software/matita/library/nat/pi_p.ma
index 93f127372..0c5e0d701 100644
--- a/helm/software/matita/library/nat/pi_p.ma
+++ b/helm/software/matita/library/nat/pi_p.ma
@@ -198,17 +198,16 @@ theorem le_pi_p:
 (\forall i. i < n \to p i = true \to g1 i \le g2 i ) \to 
 pi_p n p g1 \le pi_p n p g2.
 intros.
-generalize in match H.
-elim n
+elim n in H ⊢ %
   [apply le_n.
   |apply (bool_elim ? (p n1));intros
     [rewrite > true_to_pi_p_Sn
       [rewrite > true_to_pi_p_Sn in ⊢ (? ? %)
         [apply le_times
-          [apply H2[apply le_n|assumption]
-          |apply H1.
+          [apply H1[apply le_n|assumption]
+          |apply H.
            intros.
-           apply H2[apply le_S.assumption|assumption]
+           apply H1[apply le_S.assumption|assumption]
           ]
         |assumption
         ]
@@ -216,9 +215,9 @@ elim n
       ]
     |rewrite > false_to_pi_p_Sn
       [rewrite > false_to_pi_p_Sn in ⊢ (? ? %)
-        [apply H1.
+        [apply H.
          intros.
-         apply H2[apply le_S.assumption|assumption]
+         apply H1[apply le_S.assumption|assumption]
         |assumption
         ]
       |assumption