Let x0 of type ι be given.
Apply unknownprop_be33d753151483c7bac1e70b0036b153d449838792ed17caa64a7328dfc698e0 with
minus_SNo (28f8d.. x0),
minus_SNo (d634d.. x0) leaving 2 subgoals.
Apply SNo_minus_SNo with
28f8d.. x0.
Apply unknownprop_62ffbce17a1080b510b3d10f88e78f4b8e9088a2c54409ce0c70e91f74a9fd08 with
x0.
The subproof is completed by applying H0.
Apply SNo_minus_SNo with
d634d.. x0.
Apply unknownprop_f319423ed101339f42129d35c36f78ec84ab916352e52ec279686150bcbdfec5 with
x0.
The subproof is completed by applying H0.