Let x0 of type ι → ι → ο be given.
Let x1 of type ι → ι → ο be given.
Let x2 of type ι → ι → ο be given.
Let x3 of type (ι → ι → ο) → ι → ι → ο be given.
Assume H0: ∀ x4 : ι → ι → ο . ∀ x5 x6 . x0 x5 x6 ⟶ x3 x4 x5 x6.
Assume H1: ∀ x4 : ι → ι → ο . ∀ x5 x6 . x4 x5 x6 ⟶ x3 x4 x5 x6.
Assume H3:
∀ x4 : ι → ι → ο . ∀ x5 x6 . ∀ x7 : ι → ι . f6435.. x5 ⟶ x3 x4 x6 32d20.. ⟶ (∀ x8 . x3 (a603a.. x4 x8 x6) (x7 x8) x5) ⟶ x3 x4 (d7cf0.. x6 x7) x5.
Assume H4:
∀ x4 : ι → ι → ο . ∀ x5 x6 x7 . ∀ x8 : ι → ι . x3 x4 x5 (d7cf0.. x7 x8) ⟶ x3 x4 x6 x7 ⟶ x3 x4 (57d6a.. x5 x6) (x8 x6).
Assume H6:
∀ x4 : ι → ι → ο . ∀ x5 x6 . ∀ x7 x8 : ι → ι . f6435.. x5 ⟶ x3 x4 (d7cf0.. x6 x8) x5 ⟶ (∀ x9 . x3 (a603a.. x4 x9 x6) (x7 x9) (x8 x9)) ⟶ x3 x4 (bcddf.. x6 x7) (d7cf0.. x6 x8).
Assume H7:
∀ x4 : ι → ι → ο . ∀ x5 x6 x7 x8 x9 . f6435.. x5 ⟶ x3 x4 x6 x7 ⟶ x3 x4 x8 x5 ⟶ d3ec1.. x1 x7 x9 ⟶ d3ec1.. x1 x8 x9 ⟶ x3 x4 x6 x8.
The subproof is completed by applying H2 with x2.