Let x0 of type ι be given.
Apply unknownprop_942959aad6790cf3a71a2f8f2b9ffc552b42fb28a7f163a4f5e7e7842fdbd934 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.