| ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . nat_p x2 ⟶ equip x0 (ordsucc x2) ⟶ ∀ x3 . equip x3 x2 ⟶ ∀ x4 : ι → ι . (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x0 ⟶ x1 x6 x5 ⟶ x6 = x4 x5) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ x4 x5 = x4 x6 ⟶ x5 = x6) ⟶ ∀ x5 : ο . (∀ x6 . and (x6 ∈ x0) (∀ x7 . x7 ∈ x3 ⟶ not (x1 x6 x7)) ⟶ x5) ⟶ x5 |
|