(* NATURALI *)
(* ******** *)
-nlemma nat_destruct : ∀n1,n2:nat.S n1 = S n2 → n1 = n2.
+nlemma nat_destruct_S_S : ∀n1,n2:nat.S n1 = S n2 → n1 = n2.
#n1; #n2; #H;
nchange with (match S n2 with [ O ⇒ False | S a ⇒ n1 = a ]);
nrewrite < H;
nnormalize;
##[ ##1: #H1; nelim (nat_destruct_S_0 ? H1)
##| ##2: #n4; #H1;
- napply (H n4 (nat_destruct ?? H1))
+ napply (H n4 (nat_destruct_S_S ?? H1))
##]
##]
nqed.