Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Claim L3: ∀ x5 : ι → ο . x5 y4 ⟶ x5 y3
Let x5 of type ι → ο be given.
Claim L4: ∀ x8 : ι → ο . x8 y7 ⟶ x8 y6
Let x8 of type ι → ο be given.
set y9 to be λ x9 . x8
Apply mul_CSNo_com with
x5,
y6,
λ x10 x11 . y9 (mul_CSNo y4 x10) (mul_CSNo y4 x11) leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H4.
set y8 to be λ x8 . y7
Apply L4 with
λ x9 . y8 x9 y7 ⟶ y8 y7 x9 leaving 2 subgoals.
Assume H5: y8 y7 y7.
The subproof is completed by applying H5.
Apply mul_CSNo_assoc with
x5,
y7,
y6,
λ x9 . y8 leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
The subproof is completed by applying H2.
Claim L5: ∀ x11 : ι → ο . x11 y10 ⟶ x11 y9
Let x11 of type ι → ο be given.
set y12 to be λ x12 . x11
Apply mul_CSNo_com with
y7,
y9,
λ x13 x14 . y12 (mul_CSNo x13 y8) (mul_CSNo x14 y8) leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
set y11 to be λ x11 . y10
Apply L5 with
λ x12 . y11 x12 y10 ⟶ y11 y10 x12 leaving 2 subgoals.
Assume H6: y11 y10 y10.
The subproof is completed by applying H6.
set y12 to be λ x12 . y11
Apply mul_CSNo_assoc with
y10,
y8,
y9,
λ x13 x14 . y12 x14 x13 leaving 4 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying L5.
Let x5 of type ι → ι → ο be given.
Apply L3 with
λ x6 . x5 x6 y4 ⟶ x5 y4 x6.
Assume H4: x5 y4 y4.
The subproof is completed by applying H4.