X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fassembly%2Ftest.ma;h=1fd030efb1bb998c0302fdb3bab8c8f7695ef905;hb=d27cfdc825df15aade7edd457b08ee614d44aa32;hp=894e1bc96cca0a1702b71c46d354e23dfff5761a;hpb=d4383305e3d0fae68326d9f078b28d58b8e1f94a;p=helm.git

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 ≝