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