From c02d3479aa43b1ddc03c1af111295151acc30d43 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 2 Apr 2008 09:30:32 +0000 Subject: [PATCH] removed dummy rewrite --- helm/software/matita/library/nat/generic_iter_p.ma | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/helm/software/matita/library/nat/generic_iter_p.ma b/helm/software/matita/library/nat/generic_iter_p.ma index 4796ec10b..28ef391eb 100644 --- a/helm/software/matita/library/nat/generic_iter_p.ma +++ b/helm/software/matita/library/nat/generic_iter_p.ma @@ -158,8 +158,7 @@ iter_p_gen (k + n) p A g baseA plusA intros. elim k -[ rewrite < (plus_n_O n). - simplify. +[ simplify. rewrite > H in \vdash (? ? ? %). rewrite > (H1 ?). reflexivity @@ -283,8 +282,7 @@ elim n rewrite > sym_plus. rewrite > (div_plus_times ? ? ? H5). rewrite > (mod_plus_times ? ? ? H5). - rewrite > H4. - simplify.reflexivity. + reflexivity. ] | reflexivity ] @@ -366,8 +364,7 @@ elim n rewrite > sym_plus. rewrite > (div_plus_times ? ? ? H5). rewrite > (mod_plus_times ? ? ? H5). - rewrite > H4. - simplify.reflexivity. + reflexivity. ] | reflexivity ] -- 2.39.2