With this hint, it diverges.

[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..1dce8d535f0926646958a8224412065e55dc1ea3 100644 (file)
--- a/helm/software/matita/nlibrary/sets/partitions.ma
+++ b/helm/software/matita/nlibrary/sets/partitions.ma
@@ -26,6 +26,7 @@ alias symbol "eq" = "setoid eq".
 alias symbol "eq" = "setoid1 eq".
 alias symbol "eq" = "setoid eq".
 alias symbol "eq" = "setoid1 eq".
+alias symbol "eq" = "setoid eq".
 nrecord partition (A: setoid) : Type[1] ≝ 
  { support: setoid;
    indexes: qpowerclass support;
@@ -175,7 +176,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''; @;