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;
(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);