From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 26 May 2009 11:45:48 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~3946
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6901cc3ca6c2ceb1250fbfce10e632a9af1e9603;p=helm.git

...
---

diff --git a/helm/software/matita/tests/ng_tactics.ma b/helm/software/matita/tests/ng_tactics.ma
index 3bb4a6fa4..cf1bbe14a 100644
--- a/helm/software/matita/tests/ng_tactics.ma
+++ b/helm/software/matita/tests/ng_tactics.ma
@@ -23,7 +23,7 @@ nletin pippo ≝ (S m) in H: % ⊢ (???%);
 #H; nchange in match pippo in H:% with (pred (S pippo));
  nassert m:nat pippo : nat ≝ (S m) H:(m = pred (S pippo) + m) ⊢ (S m = S pippo);
 ngeneralize in match m in H:(??%?) ⊢ %;
-(* nassert m:nat pippo : nat ≝ (S m) ⊢ (nat → eq nat __1 (pippo+m) → pippo=S pippo); *)
+ nassert m:nat pippo : nat ≝ (S m) ⊢ (∀n:nat. n=(pred (S pippo)+m) → (S n)=S pippo);
 #x; #H;
  nassert m:nat pippo : nat ≝ (S m) x: nat H:(x = pred (S pippo) + m) ⊢ (S x = S pippo);
 nwhd in H: (?%? (?%?));