From: Claudio Sacerdoti Coen Date: Sun, 8 Jun 2008 17:14:43 +0000 (+0000) Subject: generalize no more required by elim X-Git-Tag: make_still_working~5058 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=47de0896ada04101d9d8e696c6aed733d7fcab37;p=helm.git 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 8c6f1db95..31b2d8bc0 100644 --- 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.