alias symbol "eq" = "setoid eq".
alias symbol "eq" = "setoid1 eq".
alias symbol "eq" = "setoid eq".
+alias symbol "eq" = "setoid1 eq".
nrecord partition (A: setoid) : Type[1] ≝
{ support: setoid;
indexes: qpowerclass support;
nlapply
(iso_nat_nat_union_uniq n s nindex (fst … (iso_nat_nat_union s xxx n))
nindex2 (snd … (iso_nat_nat_union s xxx n)) ?????)
- [##2: *; #E1; #E2; nrewrite > E1; nrewrite > E2; napply refl
- | napply le_S_S_to_le; nassumption
+ [##6: *; #E1; #E2; nrewrite > E1; nrewrite > E2; napply refl
+ |##5: napply le_S_S_to_le; nassumption
|##*: nassumption]##]
##| #x; #x'; nnormalize in ⊢ (? → ? → %); #Hx; #Hx'; #E;
- ngeneralize in match (? : ∀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') in ⊢ ?
- [##2: #i1; #i2; #i1'; #i2'; #Hi1; #Hi1'; #Hi2; #Hi2'; #E;
- ngeneralize in match (disjoint ? P (iso_f ???? f i1) (iso_f ???? f i1') ???) in ⊢ ?
+ 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');
+ ##[ #i1; #i2; #i1'; #i2'; #Hi1; #Hi1'; #Hi2; #Hi2'; #E;
+ nlapply(disjoint … P (f i1) (f i1') ???)
[##2,3: napply f_closed; nassumption
- |##4: napply ex_intro [ napply (iso_f ???? (fi i1) i2) ] napply conj
- [ napply f_closed; nassumption ##| napply (. ?‡#) [ nassumption | ##2: ##skip]
- nwhd; napply f_closed; nassumption]##]
- #E'; ngeneralize in match (? : i1=i1') in ⊢ ?
- [##2: napply (f_inj … E'); nassumption
- | #E''; nrewrite < E''; napply conj
- [ napply refl | nrewrite < E'' in E; #E'''; napply (f_inj … E''')
+ |##1: @ (fi i1 i2); @;
+ ##[ napply f_closed; nassumption ##| napply (. E‡#);
+ nwhd; napply f_closed; nassumption]##]
+ #E'; ncut(i1 = i1'); ##[ napply (f_inj … E'); nassumption; ##]
+ #E''; nrewrite < E''; @;
+ ##[ @;
+ ##| nrewrite < E'' in E; #E'''; napply (f_inj … E''')
[ nassumption | nrewrite > E''; nassumption ]##]##]
##] #K;
nelim (iso_nat_nat_union_char n s x Hx); *; #i1x; #i2x; #i3x;
nelim (iso_nat_nat_union_char n s x' Hx'); *; #i1x'; #i2x'; #i3x';
- ngeneralize in match (K … E) in ⊢ ?
- [##2,3: napply le_to_le_S_S; nassumption
- |##4,5: nassumption]
+ nlapply (K … E)
+ [##1,2: nassumption;
+ ##|##3,4:napply le_to_le_S_S; nassumption; ##]
*; #K1; #K2;
napply (eq_rect_CProp0_r ?? (λX.λ_.? = X) ?? i1x');
napply (eq_rect_CProp0_r ?? (λX.λ_.X = ?) ?? i1x);