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_4dacc39fbff2a1eb7f64c88eae888b40bdb7083a731b4cd05ad435e42f13fcba with x0, x1, x2, λ x3 x4 . x3 = add_CSNo (add_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_4dacc39fbff2a1eb7f64c88eae888b40bdb7083a731b4cd05ad435e42f13fcba with x0, x2, x1, λ x3 x4 . add_CSNo x0 (add_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 add_CSNo x0 (add_CSNo x2 x1)

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

Let x4 of type ι → ο be given.

Apply unknownprop_6df04587a59e9b54f0549c96144213d94328d0b365474f739b895e743839c817 with x2, y3, λ x5 x6 . (λ x7 . x4) (add_CSNo x1 x5) (add_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