#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: (?%? (?%?));