Let x0 of type ι be given.
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.
Apply unknownprop_be33d753151483c7bac1e70b0036b153d449838792ed17caa64a7328dfc698e0 with
minus_SNo (28f8d.. x0),
minus_SNo (d634d.. x0),
λ x1 x2 . ad280.. (add_SNo x2 (28f8d.. x0)) (add_SNo (d634d.. (ad280.. (minus_SNo (28f8d.. x0)) (minus_SNo (d634d.. x0)))) (d634d.. x0)) = 0 leaving 3 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying L2.
Apply unknownprop_a297e56f8bdca4759c242f4239a030f8b8676cee62a6758763e7f37b72905c22 with
minus_SNo (28f8d.. x0),
minus_SNo (d634d.. x0),
λ x1 x2 . ad280.. (add_SNo (minus_SNo (28f8d.. x0)) (28f8d.. x0)) (add_SNo x2 (d634d.. x0)) = 0 leaving 3 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying L2.
Apply add_SNo_minus_SNo_linv with
28f8d.. x0,
λ x1 x2 . ad280.. x2 (add_SNo (minus_SNo (d634d.. x0)) (d634d.. x0)) = 0 leaving 2 subgoals.
Apply unknownprop_62ffbce17a1080b510b3d10f88e78f4b8e9088a2c54409ce0c70e91f74a9fd08 with
x0.
The subproof is completed by applying H0.
Apply add_SNo_minus_SNo_linv with
d634d.. x0,
λ x1 x2 . ad280.. 0 x2 = 0 leaving 2 subgoals.
Apply unknownprop_f319423ed101339f42129d35c36f78ec84ab916352e52ec279686150bcbdfec5 with
x0.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_872273e895264b163d3a3b042c5d1abf262e26919401a643ccce2dcdcb6a14ef with 0.