| λ x0 . λ x1 : ι → ι . λ x2 : ι → ι → ι → ι . λ x3 x4 . ∀ x5 : ι → ι → ο . (∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . tuple_p (x1 x6) x7 ⟶ ∀ x8 : ι → ι . (∀ x9 . x9 ∈ x1 x6 ⟶ x5 (ap x7 x9) (x8 x9)) ⟶ x5 (lam 2 (λ x9 . If_i (x9 = 0) x6 x7)) (x2 x6 x7 (lam (x1 x6) x8))) ⟶ x5 x3 x4 |
|
| type |
|---|
| ι → (ι → ι) → (ι → ι → ι → ι) → ι → ι → ο |
|
|
|
|
|
|
|
|
|