Let x0 of type ι be given.
Apply unknownprop_971268af302c870c04b5ef1fd48c4c5b16e3b8cf5674d3506789dfb2d618197f with
x0.
Apply unknownprop_b5d0a0123c3a8bc9dcc2915dc24ee4bb0a510635f6946e2a5486e14fe0d606b6 with
x0,
0.
The subproof is completed by applying H0.