Let x0 of type ι be given.
Let x1 of type ι be given.
Apply H0 with
∃ x2 : ι → ι . bij x0 x1 x2.
Let x2 of type ι be given.
Apply H1 with
∃ x3 : ι → ι . bij x0 x1 x3.
Apply H2 with
(∀ x3 x4 x5 x6 . KPair_alt7 x3 x4 ∈ x2 ⟶ KPair_alt7 x5 x6 ∈ x2 ⟶ iff (x3 = x5) (x4 = x6)) ⟶ ∃ x3 : ι → ι . bij x0 x1 x3.
Assume H3:
∀ x3 . x3 ∈ x0 ⟶ ∃ x4 . and (x4 ∈ x1) (KPair_alt7 x3 x4 ∈ x2).
Assume H4:
∀ x3 . x3 ∈ x1 ⟶ ∃ x4 . and (x4 ∈ x0) (KPair_alt7 x4 x3 ∈ x2).
Let x3 of type ο be given.
Assume H9:
∀ x4 : ι → ι . and (and (∀ x5 . x5 ∈ x0 ⟶ x4 x5 ∈ x1) (∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ x4 x5 = x4 x6 ⟶ x5 = x6)) (∀ x5 . x5 ∈ x1 ⟶ ∃ x6 . and (x6 ∈ x0) (x4 x6 = x5)) ⟶ x3.
Apply H9 with
λ x4 . prim0 (λ x5 . KPair_alt7 x4 x5 ∈ x2).
Apply and3I with
∀ x4 . x4 ∈ x0 ⟶ (λ x5 . prim0 (λ x6 . KPair_alt7 x5 x6 ∈ x2)) x4 ∈ x1,
∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ (λ x6 . prim0 (λ x7 . KPair_alt7 x6 x7 ∈ x2)) x4 = (λ x6 . prim0 (λ x7 . KPair_alt7 x6 x7 ∈ x2)) x5 ⟶ x4 = x5,
∀ x4 . ... ⟶ ∃ x5 . and (x5 ∈ x0) ((λ x6 . prim0 (λ x7 . KPair_alt7 x6 x7 ∈ x2)) x5 = x4) leaving 3 subgoals.