nlapply (Hc y I); *; #index; *; #Hi1; #Hi2;
nlapply (f_sur ???? f ? Hi1); *; #nindex; *; #Hni1; #Hni2;
nlapply (f_sur ???? (fi nindex) y ?)
nlapply (Hc y I); *; #index; *; #Hi1; #Hi2;
nlapply (f_sur ???? f ? Hi1); *; #nindex; *; #Hni1; #Hni2;
nlapply (f_sur ???? (fi nindex) y ?)
- [ alias symbol "refl" = "refl".
-alias symbol "prop1" = "prop11".
-alias symbol "prop2" = "prop21 mem".
+ [ alias symbol "refl" (instance 3) = "refl".
+alias symbol "prop2" (instance 2) = "prop21".
+alias symbol "prop1" (instance 4) = "prop11".
napply (. #‡(†?));##[##2: napply Hni2 |##1: ##skip | nassumption]##]
*; #nindex2; *; #Hni21; #Hni22;
nletin xxx ≝ (plus (big_plus (minus n nindex) (λi.λ_.s (S (plus i nindex)))) nindex2);
napply (. #‡(†?));##[##2: napply Hni2 |##1: ##skip | nassumption]##]
*; #nindex2; *; #Hni21; #Hni22;
nletin xxx ≝ (plus (big_plus (minus n nindex) (λi.λ_.s (S (plus i nindex)))) nindex2);
[##2: *; #E1; #E2; nrewrite > E1; nrewrite > E2; //
| nassumption ]##]
##| #x; #x'; nnormalize in ⊢ (? → ? → %); #Hx; #Hx'; #E;
[##2: *; #E1; #E2; nrewrite > E1; nrewrite > E2; //
| nassumption ]##]
##| #x; #x'; nnormalize in ⊢ (? → ? → %); #Hx; #Hx'; #E;
- 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');
+ 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) (eq0 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; //
##[ #i1; #i2; #i1'; #i2'; #Hi1; #Hi1'; #Hi2; #Hi2'; #E;
nlapply(disjoint … P (f i1) (f i1') ???)
[##2,3: napply f_closed; //
| #x; #x'; #H; nnormalize; napply mk_iff; #K; nelim daemon]
##| #a; #a'; #H; napply conj; #x; nnormalize; #K [ nelim daemon | nelim daemon]##]
##| #x; #_; nnormalize; /3/
| #x; #x'; #H; nnormalize; napply mk_iff; #K; nelim daemon]
##| #a; #a'; #H; napply conj; #x; nnormalize; #K [ nelim daemon | nelim daemon]##]
##| #x; #_; nnormalize; /3/