Let x0 of type ι → ο be given.
Assume H1:
∀ x1 x2 . x0 x1 ⟶ x0 x2 ⟶ x0 (6b90c.. x1 x2).
Assume H3:
∀ x1 . x0 x1 ⟶ x0 (a6e19.. x1).
Assume H4:
∀ x1 . x0 x1 ⟶ x0 (2fe34.. x1).
Assume H5:
∀ x1 x2 . x0 x1 ⟶ x0 x2 ⟶ x0 (3e00e.. x1 x2).
Assume H6:
∀ x1 x2 . x0 x1 ⟶ x0 x2 ⟶ x0 (f9341.. x1 x2).
Assume H7:
∀ x1 . x0 x1 ⟶ x0 (1fa6d.. x1).
Assume H8:
∀ x1 . x0 x1 ⟶ x0 (3a365.. x1).
The subproof is completed by applying H0.