+ngeneralize in match m in H:(??%?) ⊢ %;
+ 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: (?%? (?%?));
+ nassert m:nat pippo:nat≝(S m) x:nat H:(x=S m + m) ⊢ (S x = S pippo);
+nchange in match (S ?) in H:(??%?) ⊢ (??%%) with (pred (S ?));
+ngeneralize in match H;
+napply (? H);
+nelim m in ⊢ (???(?%?) → %);
+nnormalize;
+ ##[ ncases x in H ⊢ (? → % → ?);
+ ##|
+ ##]