Let x0 of type ι be given.
Apply unknownprop_ab5523330112f607e055e625ca3ec71bcb7369b53cba9b5f845ed34015ce25b3 with
minus_SNo (28f8d.. x0),
minus_SNo (d634d.. x0) leaving 2 subgoals.
Apply real_minus_SNo with
28f8d.. x0.
Apply unknownprop_bf35ed077052d180738002d3131b9c960f2105b6fc771a9376424dc88c5accaa with
x0.
The subproof is completed by applying H0.
Apply real_minus_SNo with
d634d.. x0.
Apply unknownprop_f4589932e78557c04376dc773ac7e96363fb72f89bfabb77016339bd41fdf147 with
x0.
The subproof is completed by applying H0.