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: SNo x0.

Assume H1: SNo x1.

Assume H2: SNo x2.

Assume H3: SNo x3.

Let x4 of type ο be given.

Assume H4: ∀ x5 . and (SNo x5) (∃ x6 . and (SNo x6) (∃ x7 . and (SNo x7) (∃ x8 . and (SNo x8) (f4b0e.. x0 x1 x2 x3 = f4b0e.. x5 x6 x7 x8)))) ⟶ x4.

Apply H4 with x0.

Apply andI with SNo x0, ∃ x5 . and (SNo x5) (∃ x6 . and (SNo x6) (∃ x7 . and (SNo x7) (f4b0e.. x0 x1 x2 x3 = f4b0e.. x0 x5 x6 x7))) leaving 2 subgoals.

The subproof is completed by applying H0.

Let x5 of type ο be given.

Assume H5: ∀ x6 . and (SNo x6) (∃ x7 . and (SNo x7) (∃ x8 . and (SNo x8) (f4b0e.. x0 x1 x2 x3 = f4b0e.. x0 x6 x7 x8))) ⟶ x5.

Apply H5 with x1.

Apply andI with SNo x1, ∃ x6 . and (SNo x6) (∃ x7 . and (SNo x7) (f4b0e.. x0 x1 x2 x3 = f4b0e.. x0 x1 x6 x7)) leaving 2 subgoals.

The subproof is completed by applying H1.

Let x6 of type ο be given.

Assume H6: ∀ x7 . and (SNo x7) (∃ x8 . and (SNo x8) (f4b0e.. x0 x1 x2 x3 = f4b0e.. x0 x1 x7 x8)) ⟶ x6.

Apply H6 with x2.

Apply andI with SNo x2, ∃ x7 . and (SNo x7) (f4b0e.. x0 x1 x2 x3 = f4b0e.. x0 x1 x2 x7) leaving 2 subgoals.

The subproof is completed by applying H2.

Let x7 of type ο be given.

Assume H7: ∀ x8 . and (SNo x8) (f4b0e.. x0 x1 x2 x3 = f4b0e.. x0 x1 x2 x8) ⟶ x7.

Apply H7 with x3.

Apply andI with SNo x3, f4b0e.. x0 x1 x2 x3 = f4b0e.. x0 x1 x2 x3 leaving 2 subgoals.

The subproof is completed by applying H3.

Let x8 of type ι → ι → ο be given.

Assume H8: x8 (f4b0e.. x0 x1 x2 x3) (f4b0e.. x0 x1 x2 x3).

The subproof is completed by applying H8.

■

Proofgold Proof