Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H0: CSNo x0.

Assume H1: CSNo x1.

Assume H2: CSNo x2.

Apply unknownprop_f134758f39278620c60cfac6676dbfce170f8cc0cce849e07ba3004e259a9bbb with x0, x1, x2, λ x3 x4 . x3 = mul_CSNo (mul_CSNo x0 x2) x1 leaving 4 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

The subproof is completed by applying H2.

Apply unknownprop_f134758f39278620c60cfac6676dbfce170f8cc0cce849e07ba3004e259a9bbb with x0, x2, x1, λ x3 x4 . mul_CSNo x0 (mul_CSNo x1 x2) = x3 leaving 4 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H2.

The subproof is completed by applying H1.

set y3 to be mul_CSNo x0 (mul_CSNo x2 x1)

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

Let x4 of type ι → ο be given.

Apply unknownprop_4be0565ac5b41f138f7a30d0a9f34a5d126bb341d2eeaa545aa7f0c1552b9722 with x2, y3, λ x5 x6 . (λ x7 . x4) (mul_CSNo x1 x5) (mul_CSNo x1 x6) leaving 2 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H2.

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