Let x0 of type ι be given.
Let x1 of type (ι → ο) → ο be given.
Apply unknownprop_4418ace6d5c20f38cadb4d9e1d3d8f5879244a6578517e16de54bd58b60c0e1a with
35104.. x0 x1,
x0,
x1.
Let x2 of type ι → ι → ο be given.
The subproof is completed by applying H0.