generalize no more required before elim

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

diff --git a/helm/software/matita/library/nat/sieve.ma b/helm/software/matita/library/nat/sieve.ma
index 3525bc0b2280c92b19c7223836384714b70679aa..3f6775f605958d66c8407aa7792a255b93c49bab 100644 (file)
--- a/helm/software/matita/library/nat/sieve.ma
+++ b/helm/software/matita/library/nat/sieve.ma
@@ -50,9 +50,9 @@ lemma sieve_prime : \forall t,k,l2,l1.
             (prime p \to p \leq k \to in_list ? p (sieve_aux l1 l2 t)).
 intro.elim t 0
   [intros;cut (l2 = [])
-     [|generalize in match H2;elim l2
+     [|elim l2 in H2 ⊢ %
         [reflexivity
-        |simplify in H6;elim (not_le_Sn_O ? H6)]]
+        |simplify in H5;elim (not_le_Sn_O ? H5)]]
    simplify;split
      [assumption
      |intro;elim (H p);split;intros
@@ -216,7 +216,7 @@ definition list_of_primes \def \lambda n.\lambda l.
 lemma in_list_SSO_list_n : \forall n.2 \leq n \to in_list ? 2 (list_n n).
 intros;elim H;simplify
   [apply in_list_head
-  |generalize in match H2;elim H1;simplify;apply in_list_head]
+  |elim H1 in H2 ⊢ %;simplify;apply in_list_head]
 qed.
 
 lemma le_list_n_aux_k_k : \forall n,m,k.in_list ? n (list_n_aux m k) \to
@@ -243,9 +243,9 @@ qed.
 
 lemma le_list_n : \forall n,m.in_list ? n (list_n m) \to n \leq m.
 intros;unfold list_n in H;lapply (le_list_n_aux ? ? ? H);
-simplify in Hletin;generalize in match H;generalize in match Hletin;elim m
-   [simplify in H2;elim (not_in_list_nil ? ? H2)
-   |simplify in H2;assumption]
+simplify in Hletin;elim m in H Hletin ⊢ %
+   [simplify in H;elim (not_in_list_nil ? ? H)
+   |simplify in H;assumption]
 qed.
 
 
@@ -254,23 +254,23 @@ intros 3;elim H 0
   [intros;simplify;rewrite < plus_n_Sm in H2;simplify in H2;
    rewrite < plus_n_O in H2;rewrite < minus_n_O in H2;
    rewrite > (antisymmetric_le k n H1 H2);apply in_list_head
-  |intros 5;simplify;generalize in match H2;elim H3
+  |intros 5;simplify;elim H3 in H2 ⊢ %
      [apply in_list_head
-     |apply in_list_cons;apply H6
+     |apply in_list_cons;apply H5
         [apply le_S_S;assumption
-        |rewrite < plus_n_Sm in H7;apply H7]]]
+        |rewrite < plus_n_Sm in H6;apply H6]]]
 qed.
 
 lemma le_list_n_r : \forall n,m.S O < m \to 2 \leq n \to n \leq m \to in_list ? n (list_n m).
 intros;unfold list_n;apply le_list_n_aux_r
   [elim H;simplify
      [apply lt_O_S
-     |generalize in match H4;elim H3;
+     |elim H3 in H4 ⊢ %;
         [apply lt_O_S
         |simplify in H7;apply le_S;assumption]]
   |assumption
-  |simplify;generalize in match H2;elim H;simplify;assumption]
-qed.  
+  |simplify;elim H in H2 ⊢ %;simplify;assumption]
+qed.
 
 lemma le_length_list_n : \forall n. length ? (list_n n) \leq n.
 intro;cut (\forall n,k.length ? (list_n_aux n k) \leq (S n))