| ∀ x0 . x0 ⊆ prim4 3 ⟶ ∀ x1 . x1 ⊆ prim4 3 ⟶ (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x1 ⟶ ∃ x4 . and (x4 ∈ 3) (∃ x6 . and (x6 ∈ 3) (and (and (x4 = x6 ⟶ ∀ x8 : ο . x8) (x4 ∈ x2 = x4 ∈ x3)) (x6 ∈ x2 = x6 ∈ x3)))) ⟶ ∀ x2 : ο . (atleastp x0 1 ⟶ x2) ⟶ (atleastp x1 1 ⟶ x2) ⟶ (equip 2 x0 ⟶ equip 2 x1 ⟶ x2) ⟶ x2 |
|