Let x0 of type ι be given.
Let x1 of type ι be given.
Apply complex_mul_CSNo with
x0,
cbf48.. x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_c1d2bb8e040b6263924ed736e04413cf61ed14375ccce29094d9146c796b5b0d with
x1.
The subproof is completed by applying H1.