| ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ο . (explicit_Nats x0 x1 x2 ⟶ 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) ⟶ explicit_Nats x0 x1 x2 ⟶ x3 |
|
|
|
|
|
|
|
|
|
|