X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Fprod_lemmas.ma;h=6d666ca0dd3361eb29334a5a1d7a83df7938188b;hb=20fdd66303330e6209059e90b6a98af71ec29567;hp=0c8c6e6339f8e8cb932b90277a73b39e1b27b030;hpb=661cf1186c81c15122e0644b679795d2e6b9d389;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/prod_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/prod_lemmas.ma
index 0c8c6e633..6d666ca0d 100644
--- a/helm/software/matita/contribs/ng_assembly/freescale/prod_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/prod_lemmas.ma
@@ -51,7 +51,7 @@ nlemma pair_destruct_2 :
  napply (refl_eq ??).
 nqed.
 
-nlemma bsymmetric_eqpair :
+nlemma symmetric_eqpair :
 ∀T1,T2:Type.∀p1,p2:ProdT T1 T2.
 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
  (symmetricT T1 bool f1) →
@@ -142,7 +142,7 @@ nlemma triple_destruct_3 :
  napply (refl_eq ??).
 nqed.
 
-nlemma bsymmetric_eqtriple :
+nlemma symmetric_eqtriple :
 ∀T1,T2,T3:Type.∀p1,p2:Prod3T T1 T2 T3.
 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
  (symmetricT T1 bool f1) →
@@ -257,7 +257,7 @@ nlemma quadruple_destruct_4 :
  napply (refl_eq ??).
 nqed.
 
-nlemma bsymmetric_eqquadruple :
+nlemma symmetric_eqquadruple :
 ∀T1,T2,T3,T4:Type.∀p1,p2:Prod4T T1 T2 T3 T4.
 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
  (symmetricT T1 bool f1) →
@@ -397,7 +397,7 @@ nlemma quintuple_destruct_5 :
  napply (refl_eq ??).
 nqed.
 
-nlemma bsymmetric_eqquintuple :
+nlemma symmetric_eqquintuple :
 ∀T1,T2,T3,T4,T5:Type.∀p1,p2:Prod5T T1 T2 T3 T4 T5.
 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
  (symmetricT T1 bool f1) →