Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι be given.
Apply unknownprop_9f372588b2ceb8f59c01197f59d9126b3b6e4d0384005a5ae4b3ac804ebc30d1 with
8eacd.. x0 x1 x2,
x0,
x1,
x2.
Let x3 of type ι → ι → ο be given.
The subproof is completed by applying H0.