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 add_SNo_assoc with
x0,
x1,
x2,
λ x4 x5 . x3 x5 x4 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply CD_add_mul_distrL with
Sing 2,
SNo,
minus_SNo,
λ x0 . x0,
add_SNo,
mul_SNo leaving 11 subgoals.
The subproof is completed by applying complex_tag_fresh.
The subproof is completed by applying SNo_minus_SNo.
Let x0 of type ι be given.
The subproof is completed by applying H1.
The subproof is completed by applying SNo_add_SNo.
The subproof is completed by applying SNo_mul_SNo.
The subproof is completed by applying minus_add_SNo_distr.
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι → ι → ο be given.
The subproof is completed by applying H3.
The subproof is completed by applying L0.
The subproof is completed by applying add_SNo_com.
The subproof is completed by applying mul_SNo_distrL.
The subproof is completed by applying mul_SNo_distrR.