generalize no more required before elim

[helm.git] / helm / software / matita / library / nat / pi_p.ma

diff --git a/helm/software/matita/library/nat/pi_p.ma b/helm/software/matita/library/nat/pi_p.ma
index 93f127372410610e5147fe02c5bf3fa59a08b2c7..0c5e0d7014bda9cfcc98fb061738499b726d5211 100644 (file)
--- 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