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