Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_d5d9d085d36b1ca4854d01b78e983bcd20b298e2776d1ae6d4a1dc3393a026ac with
In x1 (Power x0),
Subq x1 x0.
The subproof is completed by applying unknownprop_b1dbf957f4f54b03a1b1c3419dc17583537a2d0e00a87457b7c8f86a89f7b555 with x0, x1.