Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Let x4 of type ι be given.
Apply unknownprop_bffa6df8e7b96b9efd8fc8e3fdaaadbd71fae4b5ece73e60fa0341dcf0b04e45 with
x1,
x2,
x3,
x4,
λ x5 x6 . mul_CSNo x0 x6 = mul_CSNo x4 (mul_CSNo x0 (mul_CSNo x1 (mul_CSNo x2 x3))) leaving 5 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Apply unknownprop_d58675f456b2a327cc37b294dd8f7a9297734ca60440fc59cc75cc79890a4904 with
x0,
x4,
mul_CSNo x1 (mul_CSNo x2 x3) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
Apply unknownprop_7d4f5457b1da346c62a95920399532c7f77f2218a9c26aaccd862de3e2c66112 with
x1,
x2,
x3 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.