...

diff --git a/helm/software/matita/tests/ng_tactics.ma b/helm/software/matita/tests/ng_tactics.ma
index a9cb8557787d1c5669ce54a66a988419af8e18e9..dff3db699b2303f50c2cc1b0e42129416be05e3b 100644 (file)
--- a/helm/software/matita/tests/ng_tactics.ma
+++ b/helm/software/matita/tests/ng_tactics.ma
@@ -18,7 +18,10 @@ ntheorem test1 : ∀n:nat.n = S n + n → S n = (S (S n)).
 #m; #H;
                                  nassert m:nat H: (m=S m + m) ⊢ (S m = S (S m));
 nletin pippo ≝ (S m) in H: % ⊢ (???%);
- nassert m:nat pippo : nat ≝ (S m) ⊢ (m = pippo + m → (S m) = (S pippo));
+            nassert m:nat pippo : nat ≝ (S m) ⊢ (m = pippo + m → S m = S pippo);
+#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);
+nwhd in H:(???%);
 STOP;
 
 nwhd in H:(???%);