| ∀ x0 : ι → ο . ∀ x1 : ι → ι . ∀ x2 : ο . (∀ x3 . (∀ x4 . (∃ x5 . and (exactly3 0) (not (x0 x4))) ⟶ ∀ x5 : ο . (∀ x6 . and (and (x0 0) (x0 x4)) (reflexive_i (λ x7 x8 . x0 x7) ⟶ and (x0 x3) (and (x0 (x1 x4)) (not (atleast6 x6)))) ⟶ x5) ⟶ x5) ⟶ x2) ⟶ x2 |
|