Let x0 of type ι → ο be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_1f07880e27f2756a4ce799ad0fbd848595988459e913b4d31da3f9930b95b381 with
707bb.. x0,
4b3e1.. x0,
x1,
x2.
The subproof is completed by applying H0.