Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι → ι be given.
Apply explicit_Nats_E with
x0,
x1,
x2,
∀ x3 : ο . (x1 ∈ x0 ⟶ (∀ x4 . x4 ∈ x0 ⟶ x2 x4 ∈ x0) ⟶ (∀ x4 . x4 ∈ x0 ⟶ x2 x4 = x1 ⟶ ∀ x5 : ο . x5) ⟶ (∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ x2 x4 = x2 x5 ⟶ x4 = x5) ⟶ (∀ x4 : ι → ο . x4 x1 ⟶ (∀ x5 . x4 x5 ⟶ x4 (x2 x5)) ⟶ ∀ x5 . x5 ∈ x0 ⟶ x4 x5) ⟶ x3) ⟶ x3.
Assume H1: x1 ∈ x0.
Assume H2: ∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x0.
Assume H3: ∀ x3 . x3 ∈ x0 ⟶ x2 x3 = x1 ⟶ ∀ x4 : ο . x4.
Assume H4: ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4.
Assume H5: ∀ x3 : ι → ο . x3 x1 ⟶ (∀ x4 . x3 x4 ⟶ x3 (x2 x4)) ⟶ ∀ x4 . x4 ∈ x0 ⟶ x3 x4.
Let x3 of type ο be given.
Assume H6: x1 ∈ x0 ⟶ (∀ x4 . x4 ∈ x0 ⟶ x2 x4 ∈ x0) ⟶ (∀ x4 . x4 ∈ x0 ⟶ x2 x4 = x1 ⟶ ∀ x5 : ο . x5) ⟶ (∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ x2 x4 = x2 x5 ⟶ x4 = x5) ⟶ (∀ x4 : ι → ο . x4 x1 ⟶ (∀ x5 . x4 x5 ⟶ x4 (x2 x5)) ⟶ ∀ x5 . x5 ∈ x0 ⟶ x4 x5) ⟶ x3.
Apply H6 leaving 5 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H5.