(no commit message)

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / nat_lemmas.ma

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 fde0972e4c9b1f3d9f32eb840ec32628681932f7..9e6b6e8a5da8a436cb16a239d3184e6d51651cf6 100644 (file)
--- a/helm/software/matita/contribs/ng_assembly/freescale/nat_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/nat_lemmas.ma
@@ -55,7 +55,7 @@ nlemma nat_destruct_S_0 : ∀n:nat.S n = O → False.
  napply I.
 nqed.
 
-nlemma bsymmetric_eqnat : boolSymmetric nat eq_nat.
+nlemma symmetric_eqnat : symmetricT nat bool eq_nat.
  nnormalize;
  #n1;
  nelim n1;
@@ -73,7 +73,7 @@ nlemma bsymmetric_eqnat : boolSymmetric nat eq_nat.
           ##| ##2: #n4; napply (H n4)
           ##]
  ##]
-nqed.  
+nqed.
 
 nlemma eq_to_eqnat : ∀n1,n2:nat.n1 = n2 → eq_nat n1 n2 = true.
  #n1;
@@ -101,12 +101,12 @@ nlemma eqnat_to_eq : ∀n1,n2:nat.(eq_nat n1 n2 = true → n1 = n2).
           nelim n2;
           nnormalize;
           ##[ ##1: #H; napply (refl_eq ??)
-          ##| ##2: #n3; #H; #H1; nelim (bool_destruct_false_true H1)
+          ##| ##2: #n3; #H; #H1; napply (bool_destruct ?? (O = S n3) H1) 
           ##]
  ##| ##2: #n2; #H; #n3; #H1;
           ncases n3 in H1:(%) ⊢ %;
           nnormalize;
-          ##[ ##1: #H1; nelim (bool_destruct_false_true H1)
+          ##[ ##1: #H1; napply (bool_destruct ?? (S n2 = O) H1)
           ##| ##2: #n4; #H1;
                    nrewrite > (H n4 H1);
                    napply (refl_eq ??)