...

[helm.git] / helm / software / matita / nlibrary / sets / partitions.ma

diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma
index 1dce8d535f0926646958a8224412065e55dc1ea3..c8898472233191c1dff4cd5a8884e266c5bb527b 100644 (file)
--- 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