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