Let x0 of type ι be given.
Apply unknownprop_f464d69bd91c28c03d265f2ad0625bfb5df947312ec20404c5a226eb83a04c05 with
0,
ordsucc x0.
The subproof is completed by applying unknownprop_57b23d51a8fd3f008aa6b3c62649eeea62b1db651c0fde93a21b8966982cf35e with x0.