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 mul_SNo_assoc with
x1,
x2,
mul_SNo x3 y4,
λ x6 . x5 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply SNo_mul_SNo with
x3,
y4 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Apply mul_SNo_assoc with
mul_SNo x1 x2,
x3,
y4,
λ x6 . x5 leaving 4 subgoals.
Apply SNo_mul_SNo 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 mul_SNo_assoc with
x2,
x3,
y4,
λ x8 x9 . (λ x10 x11 . (λ x12 . x7) (mul_SNo x10 x5) (mul_SNo 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.