| λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x3 x4 . x1 (x2 x4 x3 x3 x4 x4 x4 x4 x3 x4 x4 x3 x4 x4 x4 x4 x3 x4) (x2 x3 x4 x4 x3 x4 x4 x3 x4 x4 x4 x4 x3 x3 x4 x4 x4 x4) (x2 x3 x4 x4 x3 x4 x3 x4 x4 x3 x4 x4 x4 x4 x4 x3 x4 x4) (x2 x4 x3 x3 x4 x3 x4 x4 x4 x4 x3 x4 x4 x4 x3 x4 x4 x4) (x2 x4 x4 x4 x3 x4 x3 x3 x4 x4 x4 x3 x4 x4 x4 x4 x3 x4) (x2 x4 x4 x3 x4 x3 x4 x4 x3 x4 x4 x4 x3 x3 x4 x4 x4 x4) (x2 x4 x3 x4 x4 x3 x4 x4 x3 x3 x4 x4 x4 x4 x4 x3 x4 x4) (x2 x3 x4 x4 x4 x4 x3 x3 x4 x4 x3 x4 x4 x4 x3 x4 x4 x4) (x2 x4 x4 x3 x4 x4 x4 x3 x4 x4 x4 x4 x3 x3 x3 x4 x4 x4) (x2 x4 x4 x4 x3 x4 x4 x4 x3 x4 x4 x3 x4 x3 x4 x4 x3 x4) (x2 x3 x4 x4 x4 x3 x4 x4 x4 x4 x3 x4 x4 x4 x3 x3 x4 x4) (x2 x4 x3 x4 x4 x4 x3 x4 x4 x3 x4 x4 x4 x4 x4 x3 x3 x4) (x2 x4 x3 x4 x4 x4 x3 x4 x4 x3 x3 x4 x4 x4 x4 x4 x4 x3) (x2 x4 x4 x4 x3 x4 x4 x4 x3 x3 x4 x3 x4 x4 x4 x4 x4 x3) (x2 x4 x4 x3 x4 x4 x4 x3 x4 x4 x4 x3 x3 x4 x4 x4 x4 x3) (x2 x3 x4 x4 x4 x3 x4 x4 x4 x4 x3 x4 x3 x4 x4 x4 x4 x3) (x2 x4 x4 x4 x4 x4 x4 x4 x4 x4 x4 x4 x4 x3 x3 x3 x3 x4) |
|
| type |
|---|
| (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι |
|
|
|
|
|
|
|
|
|