| λ x0 : ι → ι → ο . λ x1 x2 . ∀ x3 : ι → ι → ο . (∀ x4 x5 . x0 x4 x5 ⟶ x3 x4 x5) ⟶ (∀ x4 . x3 x4 x4) ⟶ (∀ x4 x5 x6 x7 . x3 x4 x5 ⟶ x3 x6 x7 ⟶ x3 (57d6a.. x4 x6) (57d6a.. x5 x7)) ⟶ (∀ x4 x5 . ∀ x6 x7 : ι → ι . x3 x4 x5 ⟶ (∀ x8 . x3 (x6 x8) (x7 x8)) ⟶ x3 (bcddf.. x4 x6) (bcddf.. x5 x7)) ⟶ (∀ x4 x5 . ∀ x6 x7 : ι → ι . x3 x4 x5 ⟶ (∀ x8 . x3 (x6 x8) (x7 x8)) ⟶ x3 (d7cf0.. x4 x6) (d7cf0.. x5 x7)) ⟶ x3 x1 x2 |
|
| type |
|---|
| (ι → ι → ο) → ι → ι → ο |
|
|
|
|
|
|
|
|
|