Let x0 of type ι be given.
Apply unknownprop_448a658f20854233e5674076a5735fdbf479ccb6b261cbee06c64303a4bade9b with
x0.
Apply unknownprop_c213ff287d87049b1e6a47a232f87c366800922741a9eeadb1d3ac2fbadaf052 with
x0.
The subproof is completed by applying H0.