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