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