Let x0 of type ι be given.
Apply unknownprop_1a52e19bf4045e8e446a298da7dba8c076ee67253cdcf7b15e893847906b7879 with
ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc x0))))))).
Apply unknownprop_1a52e19bf4045e8e446a298da7dba8c076ee67253cdcf7b15e893847906b7879 with
x0.
The subproof is completed by applying H0.