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