From 2a5b8e5ca14aebf73dbd7532c1ac92ce9bcc895d Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 16 Jul 2007 16:10:40 +0000
Subject: [PATCH] Last daemon killed :-)

---
 helm/software/matita/library/assembly/test.ma | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

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 ≝
-- 
2.39.2