...

diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma
index 40ecd43b43ec88377f22796f37a77555cfb54c53..7affc517f79d26aaa5dfcf06463ecf7881816ed0 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;
@@ -136,7 +137,7 @@ nlemma partition_splits_card:
     (isomorphism ?? (Nat_ (big_plus n (λi.λ_.s i))) (Full_set A)).
 #A; #P; #Sn; ncases Sn
   [ #s; #f; #fi;
-    ngeneralize in match (covers ? P) in ⊢ ?; *; #_; #H;
+    nlapply (covers ? P); *; #_; #H;
     (*
     nlapply
      (big_union_preserves_iso ??? (indexes A P) (Nat_ O) (λx.class ? P x) f);