Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_e725f4e8e0c2b2b281976dec66f3ecd05466034c80c4b6357cde64cb8522d0a0 with
x0,
41fb9.. x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_3d437c63584213d7f889f1450e4056f88d3d75cf1cdf393fd727d5bf2eea1e95 with
x1.
The subproof is completed by applying H1.