From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 18 Sep 2009 15:32:45 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~3456
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=41068e795dcb5fd0e2f87d755d7f12b3cbb0f79b;p=helm.git

...
---

diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma
index 40ecd43b4..7affc517f 100644
--- 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);