Let x0 of type ι be given.

Assume H0: 8c189.. x0.

Apply H0 with 1eb0a.. x0.

Let x1 of type ι be given.

Assume H1: (λ x2 . and (SNo x2) (∃ x3 . and (SNo x3) (∃ x4 . and (SNo x4) (∃ x5 . and (SNo x5) (x0 = f4b0e.. x2 x3 x4 x5))))) x1.

Apply H1 with 1eb0a.. x0.

Assume H2: SNo x1.

Assume H3: ∃ x2 . and (SNo x2) (∃ x3 . and (SNo x3) (∃ x4 . and (SNo x4) (x0 = f4b0e.. x1 x2 x3 x4))).

Apply H3 with 1eb0a.. x0.

Let x2 of type ι be given.

Assume H4: (λ x3 . and (SNo x3) (∃ x4 . and (SNo x4) (∃ x5 . and (SNo x5) (x0 = f4b0e.. x1 x3 x4 x5)))) x2.

Apply H4 with 1eb0a.. x0.

Assume H5: SNo x2.

Assume H6: ∃ x3 . and (SNo x3) (∃ x4 . and (SNo x4) (x0 = f4b0e.. x1 x2 x3 x4)).

Apply H6 with 1eb0a.. x0.

Let x3 of type ι be given.

Assume H7: (λ x4 . and (SNo x4) (∃ x5 . and (SNo x5) (x0 = f4b0e.. x1 x2 x4 x5))) x3.

Apply H7 with 1eb0a.. x0.

Assume H8: SNo x3.

Assume H9: ∃ x4 . and (SNo x4) (x0 = f4b0e.. x1 x2 x3 x4).

Apply H9 with 1eb0a.. x0.

Let x4 of type ι be given.

Assume H10: (λ x5 . and (SNo x5) (x0 = f4b0e.. x1 x2 x3 x5)) x4.

Apply H10 with 1eb0a.. x0.

Assume H11: SNo x4.

Assume H12: x0 = f4b0e.. x1 x2 x3 x4.

Let x5 of type ο be given.

Assume H13: ∀ x6 . and (SNo x6) (∃ x7 . and (SNo x7) (∃ x8 . and (SNo x8) (∃ x9 . and (SNo x9) (∃ x10 . and (SNo x10) (∃ x11 . and (SNo x11) (∃ x12 . and (SNo x12) (∃ x13 . and (SNo x13) (x0 = bbc71.. x6 x7 x8 x9 x10 x11 x12 x13)))))))) ⟶ x5.

Apply H13 with x1.

Apply andI with SNo x1, ∃ x6 . and (SNo x6) (∃ x7 . and (SNo x7) (∃ x8 . and (SNo x8) (∃ x9 . and (SNo x9) (∃ x10 . and (SNo x10) (∃ x11 . and (SNo x11) (∃ x12 . and (SNo x12) (x0 = bbc71.. x1 x6 x7 x8 x9 x10 x11 x12))))))) leaving 2 subgoals.

The subproof is completed by applying H2.

Let x6 of type ο be given.

Assume H14: ∀ x7 . and (SNo x7) (∃ x8 . and (SNo x8) ...) ⟶ x6.

...

■

Proofgold Proof