freescale porting to ng, work in progress

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

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 0c8c6e6339f8e8cb932b90277a73b39e1b27b030..6d666ca0dd3361eb29334a5a1d7a83df7938188b 100644 (file)
--- 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) →