Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Apply unknownprop_15eb5b285a226a5656174d3a9de3f1e64f419838ace8340d1f9ea4f413ff2b14 with
x1,
x2,
x3,
λ x4 x5 . add_CSNo x0 x5 = add_CSNo x3 (add_CSNo x0 (add_CSNo x1 x2)) leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Apply unknownprop_da96b87d1828fc8ba863b6e04bdabe0039a91c2aa965c2060e150e0d03b88cbb with
x0,
x3,
add_CSNo x1 x2 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
Apply CSNo_add_CSNo with
x1,
x2 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.