generalize no more useful for elim

[helm.git] / helm / software / matita / library / decidable_kit / decidable.ma

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 ? ?));