From 47de0896ada04101d9d8e696c6aed733d7fcab37 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 8 Jun 2008 17:14:43 +0000 Subject: [PATCH] generalize no more required by elim --- helm/software/matita/library/Q/inv.ma | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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. -- 2.39.2