nassert m:nat pippo : nat ≝ (S m) ⊢ (m = pippo + m → S m = S pippo);
#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);
nassert m:nat pippo : nat ≝ (S m) ⊢ (m = pippo + m → S m = S pippo);
#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);