- hExtlib: new function "list_assoc_all"

[helm.git] / helm / software / matita / tests / ng_tactics.ma

diff --git a/helm/software/matita/tests/ng_tactics.ma b/helm/software/matita/tests/ng_tactics.ma
index a9cb8557787d1c5669ce54a66a988419af8e18e9..629c9990920b6d32c370c731d30a54323fe874f3 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);
+ngeneralize in match m in ⊢ %; (* BUG *)
 STOP;
 
 nwhd in H:(???%);