Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H0: SNo x0.

Assume H1: SNo x1.

Assume H2: SNo x2.

set y3 to be mul_SNo x2 (mul_SNo x0 x1)

Claim L3: ∀ x4 : ι → ο . x4 y3 ⟶ x4 (mul_SNo x0 (mul_SNo x1 x2))

Let x4 of type ι → ο be given.

Assume H3: x4 (mul_SNo y3 (mul_SNo x1 x2)).

set y5 to be mul_SNo x1 (mul_SNo y3 x2)

Claim L4: ∀ x6 : ι → ο . x6 y5 ⟶ x6 (mul_SNo x1 (mul_SNo x2 y3))

Let x6 of type ι → ο be given.

Apply mul_SNo_com with y3, x4, λ x7 x8 . (λ x9 . x6) (mul_SNo x2 x7) (mul_SNo x2 x8) leaving 2 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H2.

set y6 to be λ x6 . y5

Apply L4 with λ x7 . y6 x7 y5 ⟶ y6 y5 x7 leaving 2 subgoals.

Assume H5: y6 y5 y5.

The subproof is completed by applying H5.

Apply mul_SNo_assoc with y3, y5, x4, λ x7 . y6 leaving 4 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H3.

The subproof is completed by applying H2.

set y7 to be mul_SNo (mul_SNo y5 y3) x4

Claim L5: ∀ x8 : ι → ο . x8 y7 ⟶ x8 (mul_SNo (mul_SNo y3 y5) x4)

Let x8 of type ι → ο be given.

Apply mul_SNo_com with x4, y6, λ x9 x10 . (λ x11 . x8) (mul_SNo x9 y5) (mul_SNo x10 y5) leaving 2 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H3.

set y8 to be λ x8 . y7

Apply L5 with λ x9 . y8 x9 y7 ⟶ y8 y7 x9 leaving 2 subgoals.

Assume H6: y8 y7 y7.

The subproof is completed by applying H6.

Apply mul_SNo_assoc with y7, y5, y6, λ x9 x10 . (λ x11 . y8) x10 x9 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 x4 of type ι → ι → ο be given.

Apply L3 with λ x5 . x4 x5 y3 ⟶ x4 y3 x5.

Assume H4: x4 y3 y3.

The subproof is completed by applying H4.

■

Proofgold Proof