From 1ceab612eaa241f09a60073fc8a58acac6f35a37 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 16 Apr 2009 15:28:37 +0000 Subject: [PATCH] ... --- helm/software/matita/tests/ng_tactics.ma | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/helm/software/matita/tests/ng_tactics.ma b/helm/software/matita/tests/ng_tactics.ma index a9cb85577..dff3db699 100644 --- 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:(???%); -- 2.39.2