| λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 : ι → ι . λ x5 : ι → ι → ι → ι . λ x6 x7 : ι → ι . and (and (MetaNatTrans_strict x0 x1 x2 x3 x0 x1 x2 x3 (λ x8 . x8) (λ x8 x9 x10 . x10) x4 x5 x6) (MetaNatTrans_strict x0 x1 x2 x3 x0 x1 x2 x3 (λ x8 . x4 (x4 x8)) (λ x8 x9 x10 . x5 (x4 x8) (x4 x9) (x5 x8 x9 x10)) x4 x5 x7)) (MetaMonad x0 x1 x2 x3 x4 x5 x6 x7) |
|
| type |
|---|
| (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι) → (ι → ι → ι → ι) → (ι → ι) → (ι → ι) → ο |
|
|
|
|
|
|
|
|
|