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 x5 of type ι → ο be given.
Apply unknownprop_f134758f39278620c60cfac6676dbfce170f8cc0cce849e07ba3004e259a9bbb with
x1,
x2,
mul_CSNo x3 y4,
λ x6 . x5 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_3ecd982cbc53bc522aff3fa68eac8a88bfce787ef3776f0dfe2618ef278e2daf with
x3,
y4 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Apply unknownprop_f134758f39278620c60cfac6676dbfce170f8cc0cce849e07ba3004e259a9bbb with
mul_CSNo x1 x2,
x3,
y4,
λ x6 . x5 leaving 4 subgoals.
Apply unknownprop_3ecd982cbc53bc522aff3fa68eac8a88bfce787ef3776f0dfe2618ef278e2daf with
x1,
x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Let x7 of type ι → ο be given.
Apply unknownprop_f134758f39278620c60cfac6676dbfce170f8cc0cce849e07ba3004e259a9bbb with
x2,
x3,
y4,
λ x8 x9 . (λ x10 x11 . (λ x12 . x7) (mul_CSNo x10 x5) (mul_CSNo x11 x5)) x9 x8 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
set y7 to be λ x7 . y6
Apply L5 with
λ x8 . y7 x8 y6 ⟶ y7 y6 x8 leaving 2 subgoals.
Assume H6: y7 y6 y6.
The subproof is completed by applying H6.
The subproof is completed by applying L5.
Let x5 of type ι → ι → ο be given.
Apply L4 with
λ x6 . x5 x6 y4 ⟶ x5 y4 x6.
Assume H5: x5 y4 y4.
The subproof is completed by applying H5.