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