Does not compile! Wrong unification hint?

[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 c1092c497cb355e766a188c8f3c59b1862f8c961..80648f4eacddb68f3207b233654d5d7416db18ce 100644 (file)
--- a/helm/software/matita/nlibrary/sets/partitions.ma
+++ b/helm/software/matita/nlibrary/sets/partitions.ma
@@ -19,17 +19,10 @@ include "nat/minus.ma".
 include "datatypes/pairs.ma".
 
 alias symbol "eq" = "setoid eq".
-
-alias symbol "eq" = "setoid1 eq".
-alias symbol "eq" = "setoid 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
@@ -175,7 +168,8 @@ napply (. #‡(†?));##[##2: napply Hni2 |##1: ##skip | nassumption]##]
        nlapply(disjoint … P (f i1) (f i1') ???)
        [##2,3: napply f_closed; nassumption
        |##1: @ (fi i1 i2); @;
-         ##[ napply f_closed; nassumption ##| napply (. E‡#);
+         ##[ napply f_closed; nassumption ##| alias symbol "refl" = "refl1".
+napply (. E‡#);
              nwhd; napply f_closed; nassumption]##]
       #E'; ncut(i1 = i1'); ##[ napply (f_inj … E'); nassumption; ##]
       #E''; nrewrite < E''; @;