Let x0 of type ι be given.
Apply unknownprop_fa66e3d1737b2c05fa4008399b4c740ee88bf9334c6b435957b41684dfedfe51 with
1ad11.. 4a7ef.. x0.
Let x1 of type ι be given.
Apply unknownprop_da3368fefc81e401e6446c98c0c04ab87d76d6f97c47fe5fd07c1e3c2f00ef6a with
x1.
Apply unknownprop_f3a4771d3d9a8514b2ad16b328a764b0ce93421ae4df5a6923d3e167d035e33a with
4a7ef..,
x0,
x1.
The subproof is completed by applying H0.