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