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