Let x0 of type ι be given.
Apply unknownprop_cc8f63ddfbec05087d89028647ba2c7b89da93a15671b61ba228d6841bbab5e9 with
x0,
ordsucc x0.
The subproof is completed by applying unknownprop_b2bebb8105f29e822888ab2d4b10db11282fc91a7326e3993f508ffc07b3af08 with x0.