Let x0 of type ι be given.
Apply unknownprop_85bf7bdeedcc3e8cb267976cf1d04e204174cbf9a96b7acfbf556d3381ed84d4 with
x0.
Apply unknownprop_30833a9978e304b25ffd59c347245315985872140acc9e441a97543a28184d79 with
4a7ef..,
09364.. x0.
The subproof is completed by applying H0.