| λ x0 : (ι → ο) → ο . λ x1 : (ι → ι → ο) → ο . λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . λ x12 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x13 . ap (ap (x12 (x12 x2 x8 x10 x6 x5 x9 x3 x7 x4 x11) (x12 x3 x2 x4 x5 x11 x8 x7 x10 x9 x6) (x12 x4 x5 x2 x3 x7 x6 x9 x8 x11 x10) (x12 x5 x9 x8 x2 x10 x11 x4 x3 x6 x7) (x12 x6 x10 x9 x11 x2 x7 x8 x4 x3 x5) (x12 x7 x3 x5 x4 x6 x2 x11 x9 x10 x8) (x12 x8 x7 x6 x10 x4 x3 x2 x11 x5 x9) (x12 x9 x6 x11 x7 x3 x5 x10 x2 x8 x4) (x12 x10 x11 x7 x8 x9 x4 x5 x6 x2 x3) (x12 x11 x4 x3 x9 x8 x10 x6 x5 x7 x2)) x13) |
|
| type |
|---|
| ((ι → ο) → ο) → ((ι → ι → ο) → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι |
|
|
|
|
|
|
|
|
|