generalize no more required by elim

diff --git a/helm/software/matita/library/Q/inv.ma b/helm/software/matita/library/Q/inv.ma
index 8c6f1db95ecffd4d98e08768f28fc04564a1c92e..31b2d8bc006479da0c1a0798c4343688683dc08d 100644 (file)
--- a/helm/software/matita/library/Q/inv.ma
+++ b/helm/software/matita/library/Q/inv.ma
@@ -76,7 +76,7 @@ theorem is_positive_enumerator_Qinv:
  lapply (is_positive_denominator_Qinv (Qinv q));
   [ rewrite > Qinv_Qinv in Hletin;
     assumption
-  | generalize in match H; elim q; assumption]
+  | elim q in H ⊢ %; assumption]
 qed.
 
 theorem is_negative_enumerator_Qinv:
@@ -85,5 +85,5 @@ theorem is_negative_enumerator_Qinv:
  lapply (is_negative_denominator_Qinv (Qinv q));
   [ rewrite > Qinv_Qinv in Hletin;
     assumption
-  | generalize in match H; elim q; assumption]
+  | elim q in H ⊢ %; assumption]
 qed.