include "nat/minus.ma".
include "datatypes/pairs.ma".
-alias symbol "eq" = "setoid eq".
-alias symbol "eq" = "setoid1 eq".
+alias symbol "eq" (instance 7) = "setoid1 eq".
nrecord partition (A: setoid) : Type[1] ≝
{ support: setoid;
indexes: ext_powerclass support;
ncases (ltb_cases m (s (S n'))); *; #H1; #H2; nrewrite > H2;
nwhd in ⊢ (let p ≝ % in ?); nwhd
[ napply conj [napply conj
- [ nwhd in ⊢ (????(?(?%(λ_.λ_:(??%).?))%)); nrewrite > (minus_canc n'); napply refl
+ [ nwhd in ⊢ (???(?(?%(λ_.λ_:(??%).?))%)); nrewrite > (minus_canc n'); napply refl
| nnormalize; napply le_n]
##| nnormalize; nassumption ]
##| nchange in H with (m < s (S n') + big_plus (S n') (λi.λ_.s i));
|@
[nrewrite > (split_big_plus …); ##[##2:napply ad_hoc11;##|##3:##skip]
nrewrite > (ad_hoc12 …); ##[##2: nassumption]
- nwhd in ⊢ (????(?(??%)?));
+ nwhd in ⊢ (???(?(??%)?));
nrewrite > (ad_hoc13 …);##[##2: nassumption]
napply ad_hoc14 [ napply not_lt_to_le; nassumption ]
nwhd in ⊢ (???(?(??%)?));
|##5: napply le_S_S_to_le; nassumption
|##*: nassumption]##]
##| #x; #x'; nnormalize in ⊢ (? → ? → %); #Hx; #Hx'; #E;
- ncut(∀i1,i2,i1',i2'. i1 ∈ Nat_ (S n) → i1' ∈ Nat_ (S n) → i2 ∈ pc ? (Nat_ (s i1)) → i2' ∈ pc ? (Nat_ (s i1')) → eq_rel (carr A) (eq A) (iso_f ???? (fi i1) i2) (iso_f ???? (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) (eq 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; nassumption
[ napply (quotient ? R)
| napply Full_set
| napply mk_unary_morphism1
- [ #a; napply mk_qpowerclass
+ [ #a; napply mk_ext_powerclass
[ napply {x | 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]##]