Let x0 of type ι be given.
Apply unknownprop_8aec7aa3dfe2dc8cbf1366cb9f5d8ab2c4ceeb7b1cd3cc933b26d92d53269901 with
2,
x0,
x0.
The subproof is completed by applying unknownprop_678f269783f56623b590ce1d631178bc95b1ef296ba955ebeddcd0dc31626e86 with x0.