| λ x0 x1 x2 . ∀ x3 : ι → ι → ο . (∀ x4 x5 . x3 x4 x5 ⟶ x3 x5 x4) ⟶ or (∃ x4 . and (x4 ⊆ x2) (and (atleastp x0 x4) (∀ x6 . x6 ∈ x4 ⟶ ∀ x7 . x7 ∈ x4 ⟶ (x6 = x7 ⟶ ∀ x8 : ο . x8) ⟶ x3 x6 x7))) (∃ x4 . and (x4 ⊆ x2) (and (atleastp x1 x4) (∀ x6 . x6 ∈ x4 ⟶ ∀ x7 . x7 ∈ x4 ⟶ (x6 = x7 ⟶ ∀ x8 : ο . x8) ⟶ not (x3 x6 x7)))) |
|