Let x0 of type ι be given.
Apply mul_SNo_com_4_inner_mid with
2,
x0,
2,
x0,
λ x1 x2 . mul_SNo 4 (mul_SNo x0 x0) = x2 leaving 5 subgoals.
The subproof is completed by applying SNo_2.
The subproof is completed by applying H0.
The subproof is completed by applying SNo_2.
The subproof is completed by applying H0.
Apply unknownprop_44c5ad117e7e64261599b655dea9987852fea6a0c917a86782f3919004220c6a with
λ x1 x2 . mul_SNo 4 (mul_SNo x0 x0) = mul_SNo x2 (mul_SNo x0 x0).
Let x2 of type ι → ι → ο be given.
Assume H1: x2 y1 y1.
The subproof is completed by applying H1.