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