X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Fnat_lemmas.ma;h=70b9bbbb90418046b7ec8fe8f7a5dc75ec06d288;hb=20fdd66303330e6209059e90b6a98af71ec29567;hp=9e6b6e8a5da8a436cb16a239d3184e6d51651cf6;hpb=661cf1186c81c15122e0644b679795d2e6b9d389;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/nat_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/nat_lemmas.ma
index 9e6b6e8a5..70b9bbbb9 100644
--- a/helm/software/matita/contribs/ng_assembly/freescale/nat_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/nat_lemmas.ma
@@ -31,7 +31,7 @@ include "freescale/nat.ma".
 (* 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;
@@ -89,7 +89,7 @@ nlemma eq_to_eqnat : ∀n1,n2:nat.n1 = n2 → eq_nat n1 n2 = true.
           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.