generalize no more useful for elim

diff --git a/helm/software/matita/library/decidable_kit/decidable.ma b/helm/software/matita/library/decidable_kit/decidable.ma
index dff89f8d35cc5d5d46a8539a9f8980b57fe2f70f..9c2f8890b59d8a6cf294f693b27ba4dbda7bf194 100644 (file)
--- a/helm/software/matita/library/decidable_kit/decidable.ma
+++ b/helm/software/matita/library/decidable_kit/decidable.ma
@@ -170,7 +170,7 @@ intros (m n); apply bool_to_eq; split;
 [1: intros; cases (b2pT ? ? (orbP ? ?) H); [1: apply ltbW; assumption]
     rewrite > (eqb_true_to_eq ? ? H1); simplify; 
     rewrite > leb_refl; reflexivity  
-|2: generalize in match m; clear m; elim n 0;
+|2: elim n in m ⊢ % 0;
     [1: simplify; intros; cases n1; reflexivity;
     |2: intros 1 (m); elim m 0;
         [1: intros; apply (p2bT ? ? (orbP ? ?));

diff --git a/helm/software/matita/library/decidable_kit/list_aux.ma b/helm/software/matita/library/decidable_kit/list_aux.ma
index a38d5eb83cc499063b1349003b2904e911925b10..a7db00c7278292d471ece6424af61ef19ba95062 100644 (file)
--- a/helm/software/matita/library/decidable_kit/list_aux.ma
+++ b/helm/software/matita/library/decidable_kit/list_aux.ma
@@ -58,8 +58,7 @@ cases c; intros (H); [ apply reflect_true | apply reflect_false ]
   apply (list_ind2 ? ? ? ? ? Hl); [1: intros; reflexivity]
   simplify; intros (tl1 tl2 hd1 hd2 IH H); cases (b2pT ? ? (andbP ? ?) H);
   rewrite > (IH H2); rewrite > (b2pT ? ? (eqP d ? ?) H1); reflexivity
-| generalize in match H; clear H; generalize in match l2; clear l2;
-  elim l1 1 (l1 x1);
+| elim l1 in H l2 ⊢ % 1 (l1 x1);
    [ cases l1; simplify; [intros; destruct H | unfold Not; intros; destruct H1;]
    | intros 3 (tl1 IH l2); cases l2;
      [ unfold Not; intros; destruct H1;