...

[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 1bb482f6e1c1310b133b0f1508aee6e3857bf2b0..de29e796c47141fc80cd8659aa35a64c68e01a82 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;
@@ -81,7 +78,7 @@ ntheorem iso_nat_nat_union_char:
     ncases (ltb_cases m (s (S n'))); *; #H1; #H2; nrewrite > H2;
     nwhd in ⊢ (let p ≝ % in ?); nwhd
      [ napply conj [napply conj
-        [ nwhd in ⊢ (????(?(?%(λ_.λ_:(??%).?))%)); nrewrite > (minus_canc n'); napply refl
+        [ nwhd in ⊢ (???(?(?%(λ_.λ_:(??%).?))%)); nrewrite > (minus_canc n'); napply refl
         | nnormalize; napply le_n]
       ##| nnormalize; nassumption ]
    ##| nchange in H with (m < s (S n') + big_plus (S n') (λi.λ_.s i));
@@ -91,7 +88,7 @@ ntheorem iso_nat_nat_union_char:
         |@
          [nrewrite > (split_big_plus …); ##[##2:napply ad_hoc11;##|##3:##skip]
           nrewrite > (ad_hoc12 …); ##[##2: nassumption]
-          nwhd in ⊢ (????(?(??%)?));
+          nwhd in ⊢ (???(?(??%)?));
           nrewrite > (ad_hoc13 …);##[##2: nassumption]
           napply ad_hoc14 [ napply not_lt_to_le; nassumption ]
           nwhd in ⊢ (???(?(??%)?));