#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: (?%? (?%?));
nchange in match (S ?) in H:(??%?) ⊢ (??%%) with (pred (S ?));
ngeneralize in match H;
napply (? H);
-nelim m in ⊢ (???(?%?) → %); (*SBAGLIA UNIFICATORE*)
+nelim m in ⊢ (???(?%?) → %);
nnormalize;
##[ ncases x in H ⊢ (? → % → ?);
##|