| λ x0 x1 x2 . λ x3 x4 : ι → ι → ι . λ x5 : ι → ι → ο . λ x6 . ∀ x7 : ο . (∀ x8 . (∀ x9 : ο . (∀ x10 . and (and (natOfOrderedField_p x0 x1 x2 x3 x4 x5 x8) (natOfOrderedField_p x0 x1 x2 x3 x4 x5 x10)) (x4 x10 x6 = x8) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7 |
|
| type |
|---|
| ι → ι → ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ο) → ι → ο |
|
|
|
|
|
|
|
|
|