From: Claudio Sacerdoti Coen Date: Mon, 16 Jul 2007 16:10:40 +0000 (+0000) Subject: Last daemon killed :-) X-Git-Tag: make_still_working~6170 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2a5b8e5ca14aebf73dbd7532c1ac92ce9bcc895d;p=helm.git Last daemon killed :-) --- diff --git a/helm/software/matita/library/assembly/test.ma b/helm/software/matita/library/assembly/test.ma index 894e1bc96..1fd030efb 100644 --- a/helm/software/matita/library/assembly/test.ma +++ b/helm/software/matita/library/assembly/test.ma @@ -214,7 +214,9 @@ lemma loop_invariant': normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?); normalize in ⊢ (? ? (? (? ? ? ? ? ? (? ? % ?) ?) ?) ?); cut (y - S n = a); - [2: elim daemon | ]; + [2: rewrite > eq_minus_S_pred; + rewrite > H2; + reflexivity | ]; rewrite < Hcut; clear Hcut; clear H3; clear H2; clear a; (* instruction ADDd *) letin K ≝