From 41068e795dcb5fd0e2f87d755d7f12b3cbb0f79b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 18 Sep 2009 15:32:45 +0000 Subject: [PATCH] ... --- helm/software/matita/nlibrary/sets/partitions.ma | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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); -- 2.39.2