Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Let x3 of type ι be given.

Assume H0: CSNo x0.

Assume H1: CSNo x1.

Assume H2: CSNo x2.

Assume H3: CSNo x3.

set y4 to be add_CSNo (add_CSNo x0 (add_CSNo x1 x2)) x3

Claim L4: ∀ x5 : ι → ο . x5 y4 ⟶ x5 (add_CSNo x0 (add_CSNo x1 (add_CSNo x2 x3)))

Let x5 of type ι → ο be given.

Assume H4: x5 (add_CSNo (add_CSNo x1 (add_CSNo x2 x3)) y4).

Apply unknownprop_4dacc39fbff2a1eb7f64c88eae888b40bdb7083a731b4cd05ad435e42f13fcba with x1, x2, add_CSNo x3 y4, λ x6 . x5 leaving 4 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

Apply CSNo_add_CSNo with x3, y4 leaving 2 subgoals.

The subproof is completed by applying H2.

The subproof is completed by applying H3.

Apply unknownprop_4dacc39fbff2a1eb7f64c88eae888b40bdb7083a731b4cd05ad435e42f13fcba with add_CSNo x1 x2, x3, y4, λ x6 . x5 leaving 4 subgoals.

Apply CSNo_add_CSNo 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.

set y6 to be add_CSNo (add_CSNo x1 (add_CSNo x2 x3)) y4

Claim L5: ∀ x7 : ι → ο . x7 y6 ⟶ x7 (add_CSNo (add_CSNo (add_CSNo x1 x2) x3) y4)

Let x7 of type ι → ο be given.

Apply unknownprop_4dacc39fbff2a1eb7f64c88eae888b40bdb7083a731b4cd05ad435e42f13fcba with x2, x3, y4, λ x8 x9 . (λ x10 x11 . (λ x12 . x7) (add_CSNo x10 x5) (add_CSNo 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.

■

Proofgold Proof