Let x0 of type ι be given.
Let x1 of type ι → ι → ι → ο be given.
Assume H0:
∀ x2 . x1 c4def.. x2 x2.
Assume H1:
∀ x2 x3 x4 x5 x6 . x1 x2 x4 x5 ⟶ x1 x3 x5 x6 ⟶ x1 (6b90c.. x2 x3) x4 x6.
Assume H3:
∀ x2 x3 x4 . x1 x2 x3 x4 ⟶ x1 (a6e19.. x2) x3 (0b8ef.. x4).
Assume H4:
∀ x2 x3 x4 . x1 x2 x3 x4 ⟶ x1 (2fe34.. x2) x3 (6c5f4.. x4).
Assume H7:
∀ x2 x3 x4 x5 x6 . x1 x2 x4 x5 ⟶ x1 x3 x4 x6 ⟶ x1 (f9341.. x2 x3) x4 (cfc98.. x5 x6).
Assume H8:
∀ x2 x3 x4 x5 . x1 x2 x3 x5 ⟶ x1 (1fa6d.. x2) (cfc98.. x3 x4) x5.
Assume H9:
∀ x2 x3 x4 x5 . x1 x2 x4 x5 ⟶ x1 (3a365.. x2) (cfc98.. x3 x4) x5.
The subproof is completed by applying H0 with x0.