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