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