+ngeneralize in match m in H:(??%?) ⊢ %;
+(* nassert m:nat pippo : nat ≝ (S m) ⊢ (nat → eq nat __1 (pippo+m) → pippo=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 ⊢ (???(?%?) → %); (*SBAGLIA UNIFICATORE*)
+nnormalize;
+ ##[ ncases x in H ⊢ (? → % → ?);
+ ##|
+ ##]