instances

diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma
index 1bb482f6e1c1310b133b0f1508aee6e3857bf2b0..dde57de058ce45406b15c78e580cee79daee1ce6 100644 (file)
--- a/helm/software/matita/nlibrary/sets/partitions.ma
+++ b/helm/software/matita/nlibrary/sets/partitions.ma
@@ -18,10 +18,7 @@ include "nat/compare.ma".
 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" = "setoid1 eq".
+alias symbol "eq" (instance 7) = "setoid1 eq".
 nrecord partition (A: setoid) : Type[1] ≝ 
  { support: setoid;
    indexes: ext_powerclass support;

diff --git a/helm/software/matita/nlibrary/topology/igft2.ma b/helm/software/matita/nlibrary/topology/igft2.ma
index 4703fba8c770659fc251fe5f0cf689e3a1f64653..90a644ce92c65b8e2ad81ec9ebcc66c130a253be 100644 (file)
--- a/helm/software/matita/nlibrary/topology/igft2.ma
+++ b/helm/software/matita/nlibrary/topology/igft2.ma
@@ -30,17 +30,11 @@ nlemma cover_ind':
             napply infty; nauto; ##] 
 nqed.
 
-alias symbol "covers" = "covers".
-alias symbol "covers" = "covers set".
-alias symbol "covers" = "covers".
-alias symbol "covers" = "covers set".
-alias symbol "covers" = "covers".
-alias symbol "covers" = "covers set".
+alias symbol "covers" (instance 1) = "covers".
 nlemma cover_ind'':
  ∀A:Ax.∀U:Ω^A.∀P:A → CProp[0].
   (∀a. a ∈ U → P a) → (∀a:A.∀j:𝐈 a. 𝐂 a j ◃ U → (∀b. b ∈ 𝐂 a j → P b) → P a) →
    ∀b. b ◃ U → P b.
-   
  #A; #U; #P; nletin V ≝ {x | P x}; napply (cover_ind' … V).
 nqed.
 
@@ -96,10 +90,8 @@ nrecord memdec (A: Type[0]) (U:Ω^A) : Type[0] ≝
 
 (*********** end from Cantor ********)
 
-alias symbol "covers" = "covers".
-alias symbol "covers" = "covers".
-alias symbol "covers" = "covers set".
-alias symbol "covers" = "covers set".
+alias symbol "covers" (instance 9) = "covers".
+alias symbol "covers" (instance 8) = "covers".
 nlet rec cover_rect
  (A:uuAx) (U:Ω^(uuax A)) (memdec: memdec … U) (P:uuax A → Type[0])
   (refl: ∀a:uuax A. a ∈ U → P a)