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_83f42a9be1fb70a66754d3f1ec6766cd22411cf20e288c8e140f22d881bd2da2 with
x1,
x2,
x3,
λ x4 x5 . mul_CSNo x0 x5 = mul_CSNo x3 (mul_CSNo x0 (mul_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_d58675f456b2a327cc37b294dd8f7a9297734ca60440fc59cc75cc79890a4904 with
x0,
x3,
mul_CSNo x1 x2 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
Apply unknownprop_3ecd982cbc53bc522aff3fa68eac8a88bfce787ef3776f0dfe2618ef278e2daf with
x1,
x2 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.