update in groud_2 and models

[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 b92fe9ab3011d9bcbcb75637b51c886c43de6d05..3eea5010166d4d61c5ff51e98646fd3c8ca94e36 100644 (file)
--- a/helm/software/matita/nlibrary/sets/partitions.ma
+++ b/helm/software/matita/nlibrary/sets/partitions.ma
@@ -146,7 +146,7 @@ napply (. #‡(†?));##[##2: napply Hni2 |##1: ##skip | nassumption]##]
         [##2: *; #E1; #E2; nrewrite > E1; nrewrite > E2; //
         | nassumption ]##]
 ##| #x; #x'; nnormalize in ⊢ (? → ? → %); #Hx; #Hx'; #E;
-    ncut(∀i1,i2,i1',i2'. i1 ∈ Nat_ (S n) → i1' ∈ Nat_ (S n) → i2 ∈ Nat_ (s i1) → i2' ∈ Nat_ (s i1') → eq_rel (carr A) (eq A) (fi i1 i2) (fi i1' i2') → i1=i1' ∧ i2=i2');
+    ncut(∀i1,i2,i1',i2'. i1 ∈ Nat_ (S n) → i1' ∈ Nat_ (S n) → i2 ∈ Nat_ (s i1) → i2' ∈ Nat_ (s i1') → eq_rel (carr A) (eq0 A) (fi i1 i2) (fi i1' i2') → i1=i1' ∧ i2=i2');
     ##[ #i1; #i2; #i1'; #i2'; #Hi1; #Hi1'; #Hi2; #Hi2'; #E;
        nlapply(disjoint … P (f i1) (f i1') ???)
        [##2,3: napply f_closed; //
@@ -179,7 +179,7 @@ ndefinition partition_of_compatible_equivalence_relation:
   | napply Full_set
   | napply mk_unary_morphism1
      [ #a; napply mk_ext_powerclass
-        [ napply {x | R x a}
+        [ napply {x | rel ? R x a}
         | #x; #x'; #H; nnormalize; napply mk_iff; #K; nelim daemon]
    ##| #a; #a'; #H; napply conj; #x; nnormalize; #K [ nelim daemon | nelim daemon]##]
 ##| #x; #_; nnormalize; /3/