generalize no more required before elim

[helm.git] / helm / software / matita / library / demo / propositional_sequent_calculus.ma

diff --git a/helm/software/matita/library/demo/propositional_sequent_calculus.ma b/helm/software/matita/library/demo/propositional_sequent_calculus.ma
index d647830bff9e938afb1446cf670dab4e647fdcf3..fb5278d6bdd78d44646652e6111317dc0fe3e370 100644 (file)
--- a/helm/software/matita/library/demo/propositional_sequent_calculus.ma
+++ b/helm/software/matita/library/demo/propositional_sequent_calculus.ma
@@ -422,8 +422,7 @@ lemma same_atom_to_eq: ∀f1,f2. same_atom f1 f2 = true → f1=f2.
   [1,2:
     simplify in H;
     destruct H
-  | generalize in match H; clear H;
-    elim f2;
+  | elim f2 in H ⊢ %;
      [1,2:
        simplify in H;
        destruct H
@@ -588,16 +587,10 @@ lemma sizel_0_no_axiom_is_tautology:
  intros;
  lapply (H1 (λn.mem ? same_atom (FAtom n) l1)); clear H1;
  simplify in Hletin;  
- generalize in match Hletin; clear Hletin;
- generalize in match H2; clear H2;
- generalize in match H; clear H;
- elim l1 0;
+ elim l1 in Hletin H2 H ⊢ % 0;
   [ intros;
     simplify in H2;
-    generalize in match H2; clear H2;
-    generalize in match H1; clear H1;
-    generalize in match H; clear H;
-    elim l2 0;
+    elim l2 in H2 H1 H ⊢ % 0;
      [ intros;
        simplify in H2;
        destruct H2
@@ -677,8 +670,7 @@ lemma sizel_0_no_axiom_is_tautology:
         | assumption
         | lapply (H2 n1); clear H2;
           simplify in Hletin;
-          generalize in match Hletin; clear Hletin;
-          elim (eqb n1 n);
+          elim (eqb n1 n) in Hletin ⊢ %;
            [ simplify in H2;
              rewrite > H2;
              autobatch
@@ -693,10 +685,7 @@ lemma sizel_0_no_axiom_is_tautology:
           rewrite > eqb_n_n in H3;
           simplify in H3;
 (*
-          generalize in match H3;
-          generalize in match H1; clear H1;
-          generalize in match H; clear H;
-          elim l 0;
+          elim l in H3 H1 H ⊢ % 0;
            [ elim l2 0;
               [ intros;
                 simplify in H2;
@@ -714,9 +703,7 @@ lemma sizel_0_no_axiom_is_tautology:
                  ]
                     
                  [ autobatch
-                 | generalize in match H4; clear H4;
-                   generalize in match H2; clear H2;
-                   elim t1;
+                 | elim t1 in H4 H2 ⊢ %;
                     [
                     |
                     |