From 6901cc3ca6c2ceb1250fbfce10e632a9af1e9603 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 26 May 2009 11:45:48 +0000 Subject: [PATCH] ... --- helm/software/matita/tests/ng_tactics.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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: (?%? (?%?)); -- 2.39.2