From dc7c02d8d8678d250a99dd6d012adcd69da63b75 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 4 Oct 2009 14:43:48 +0000
Subject: [PATCH 1/1] ...

---
 helm/software/matita/nlibrary/sets/partitions.ma | 5 +++--
 helm/software/matita/nlibrary/sets/sets.ma       | 8 ++++----
 2 files changed, 7 insertions(+), 6 deletions(-)

diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma
index 1dce8d535..c88984722 100644
--- a/helm/software/matita/nlibrary/sets/partitions.ma
+++ b/helm/software/matita/nlibrary/sets/partitions.ma
@@ -27,10 +27,11 @@ alias symbol "eq" = "setoid1 eq".
 alias symbol "eq" = "setoid eq".
 alias symbol "eq" = "setoid1 eq".
 alias symbol "eq" = "setoid eq".
+alias symbol "eq" = "setoid1 eq".
 nrecord partition (A: setoid) : Type[1] ≝ 
  { support: setoid;
-   indexes: qpowerclass support;
-   class: unary_morphism1 (setoid1_of_setoid support) (qpowerclass_setoid A);
+   indexes: ext_powerclass support;
+   class: unary_morphism1 (setoid1_of_setoid support) (ext_powerclass_setoid A);
    inhabited: ∀i. i ∈ indexes → class i ≬ class i;
    disjoint: ∀i,j. i ∈ indexes → j ∈ indexes → class i ≬ class j → i = j;
    covers: big_union support ? indexes (λx.class x) = full_set A
diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index f230957a7..3cf65c118 100644
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -267,6 +267,7 @@ nlemma test: ∀A:setoid. ∀U,V:qpowerclass A. ∀x,x':setoid1_of_setoid A. x=x
  #A; #U; #V; #x; #x'; #H; #p; napply (. (H^-1‡#)); nassumption.
 nqed.
 *)
+*)
 
 ndefinition image: ∀A,B. (carr A → carr B) → Ω^A → Ω^B ≝
  λA,B:setoid.λf:carr A → carr B.λSa:Ω^A.
@@ -317,11 +318,11 @@ nlemma first_omomorphism_theorem_functions1:
 nqed.
 
 ndefinition surjective ≝
- λA,B.λS: qpowerclass A.λT: qpowerclass B.λf:unary_morphism A B.
+ λA,B.λS: ext_powerclass A.λT: ext_powerclass B.λf:unary_morphism A B.
   ∀y. y ∈ T → ∃x. x ∈ S ∧ f x = y.
 
 ndefinition injective ≝
- λA,B.λS: qpowerclass A.λf:unary_morphism A B.
+ λA,B.λS: ext_powerclass A.λf:unary_morphism A B.
   ∀x,x'. x ∈ S → x' ∈ S → f x = f x' → x = x'.
 
 nlemma first_omomorphism_theorem_functions2:
@@ -337,7 +338,7 @@ nlemma first_omomorphism_theorem_functions3:
  #A; #B; #f; nwhd; #x; #x'; #Hx; #Hx'; #K; nassumption.
 nqed.
 
-nrecord isomorphism (A, B : setoid) (S: qpowerclass A) (T: qpowerclass B) : Type[0] ≝
+nrecord isomorphism (A, B : setoid) (S: ext_powerclass A) (T: ext_powerclass B) : Type[0] ≝
  { iso_f:> unary_morphism A B;
    f_closed: ∀x. x ∈ S → iso_f x ∈ T;
    f_sur: surjective … S T iso_f;
@@ -365,4 +366,3 @@ ncheck (λA:?.
    ;
  }.
 *)
-*)
\ No newline at end of file
-- 
2.39.2