| λ x0 x1 x2 : ι → ι → ο . λ x3 x4 . ∀ x5 : (ι → ι → ο) → ι → ι → ο . (∀ x6 : ι → ι → ο . ∀ x7 x8 . x0 x7 x8 ⟶ x5 x6 x7 x8) ⟶ (∀ x6 : ι → ι → ο . ∀ x7 x8 . x6 x7 x8 ⟶ x5 x6 x7 x8) ⟶ (∀ x6 : ι → ι → ο . x5 x6 32d20.. 6915e..) ⟶ (∀ x6 : ι → ι → ο . ∀ x7 x8 . ∀ x9 : ι → ι . f6435.. x7 ⟶ x5 x6 x8 32d20.. ⟶ (∀ x10 . x5 (a603a.. x6 x10 x8) (x9 x10) x7) ⟶ x5 x6 (d7cf0.. x8 x9) x7) ⟶ (∀ x6 : ι → ι → ο . ∀ x7 x8 x9 . ∀ x10 : ι → ι . x5 x6 x7 (d7cf0.. x9 x10) ⟶ x5 x6 x8 x9 ⟶ x5 x6 (57d6a.. x7 x8) (x10 x8)) ⟶ (∀ x6 : ι → ι → ο . ∀ x7 x8 . ∀ x9 x10 : ι → ι . f6435.. x7 ⟶ x5 x6 (d7cf0.. x8 x10) x7 ⟶ (∀ x11 . x5 (a603a.. x6 x11 x8) (x9 x11) (x10 x11)) ⟶ x5 x6 (bcddf.. 236c6.. x9) (d7cf0.. x8 x10)) ⟶ (∀ x6 : ι → ι → ο . ∀ x7 x8 . ∀ x9 x10 : ι → ι . f6435.. x7 ⟶ x5 x6 (d7cf0.. x8 x10) x7 ⟶ (∀ x11 . x5 (a603a.. x6 x11 x8) (x9 x11) (x10 x11)) ⟶ x5 x6 (bcddf.. x8 x9) (d7cf0.. x8 x10)) ⟶ (∀ x6 : ι → ι → ο . ∀ x7 x8 x9 x10 x11 . f6435.. x7 ⟶ x5 x6 x8 x9 ⟶ x5 x6 x10 x7 ⟶ d3ec1.. x1 x9 x11 ⟶ d3ec1.. x1 x10 x11 ⟶ x5 x6 x8 x10) ⟶ x5 x2 x3 x4 |
|