From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 2 Apr 2008 09:30:32 +0000 (+0000)
Subject: removed dummy rewrite
X-Git-Tag: make_still_working~5471
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c02d3479aa43b1ddc03c1af111295151acc30d43;hp=68d0514bb21f373827bc3578a6b30e5fd95b6271;p=helm.git

removed dummy rewrite
---

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
       ]