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