ProdT was a perfect copy of Prod. Removed.

[helm.git] / helm / software / matita / library / algebra / CoRN / Setoids.ma

diff --git a/helm/software/matita/library/algebra/CoRN/Setoids.ma b/helm/software/matita/library/algebra/CoRN/Setoids.ma
index 982d61caf19297e62b99abb2ed35c1c98af465f3..30c8c8bd5d128ebefbfc2d212f5e7ac75f8927ac 100644 (file)
--- a/helm/software/matita/library/algebra/CoRN/Setoids.ma
+++ b/helm/software/matita/library/algebra/CoRN/Setoids.ma
@@ -215,19 +215,19 @@ qed.
 
 (* -----------------The product of setoids----------------------- *)
 
-definition prod_ap: \forall A,B : CSetoid.\forall c,d: ProdT A B. Prop \def
-\lambda A,B : CSetoid.\lambda c,d: ProdT A B.
-  ((cs_ap A (fstT A B c) (fstT A B d)) \or 
-   (cs_ap B (sndT A B c) (sndT A B d))).
-
-definition prod_eq: \forall A,B : CSetoid.\forall c,d: ProdT A B. Prop \def
-\lambda A,B : CSetoid.\lambda c,d: ProdT A B.
-  ((cs_eq A (fstT A B c) (fstT A B d)) \and 
-   (cs_eq B (sndT A B c) (sndT A B d))).
+definition prod_ap: \forall A,B : CSetoid.\forall c,d: Prod A B. Prop \def
+\lambda A,B : CSetoid.\lambda c,d: Prod A B.
+  ((cs_ap A (fst A B c) (fst A B d)) \or 
+   (cs_ap B (snd A B c) (snd A B d))).
+
+definition prod_eq: \forall A,B : CSetoid.\forall c,d: Prod A B. Prop \def
+\lambda A,B : CSetoid.\lambda c,d: Prod A B.
+  ((cs_eq A (fst A B c) (fst A B d)) \and 
+   (cs_eq B (snd A B c) (snd A B d))).
       
 
 lemma prodcsetoid_is_CSetoid: \forall A,B: CSetoid.
- is_CSetoid (ProdT A B) (prod_eq A B) (prod_ap A B).
+ is_CSetoid (Prod A B) (prod_eq A B) (prod_ap A B).
 intros.
 apply (mk_is_CSetoid ? (prod_eq A B) (prod_ap A B))
   [unfold.
@@ -301,7 +301,7 @@ qed.
 
 definition ProdCSetoid : \forall A,B: CSetoid. CSetoid \def
  \lambda A,B: CSetoid.
-  mk_CSetoid (ProdT A B) (prod_eq A B) (prod_ap A B) (prodcsetoid_is_CSetoid A B).
+  mk_CSetoid (Prod A B) (prod_eq A B) (prod_ap A B) (prodcsetoid_is_CSetoid A B).