Let x0 of type ι → ι → ο be given.
Let x1 of type ι → ι → ο be given.
Let x2 of type ι → ι → ο be given.
Let x3 of type ι be given.
Let x4 of type ι be given.
Assume H0: x0 x3 x4.
Let x5 of type (ι → ι → ο) → ι → ι → ο be given.
Assume H1: ∀ x6 : ι → ι → ο . ∀ x7 x8 . x0 x7 x8 ⟶ x5 x6 x7 x8.
Assume H2: ∀ x6 : ι → ι → ο . ∀ x7 x8 . x6 x7 x8 ⟶ x5 x6 x7 x8.
Assume H4:
∀ 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.
Assume H5:
∀ x6 : ι → ι → ο . ∀ x7 x8 x9 . ∀ x10 : ι → ι . x5 x6 x7 (d7cf0.. x9 x10) ⟶ x5 x6 x8 x9 ⟶ x5 x6 (57d6a.. x7 x8) (x10 x8).
Assume H7:
∀ 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).
Assume H8:
∀ 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.
Apply H1 with
x2,
x3,
x4.
The subproof is completed by applying H0.