[##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/