Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Apply unknownprop_85c22e88a806aabda7246f27ac458442bcb94ac25cc9a3616a68cf646d95941d with
x0,
1216a.. x0 x1.
The subproof is completed by applying unknownprop_ff2867b3bb208ef289baf197b08ab3d0f53f75a122d24e65f4370d386c16168a with x0, x1.