Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_85c22e88a806aabda7246f27ac458442bcb94ac25cc9a3616a68cf646d95941d with
x0,
1ad11.. x0 x1.
The subproof is completed by applying unknownprop_f4cb3db9b44278d291dda59763d3ebc8189ce94e5657538eeb63abd989060e4e with x0, x1.