Let x0 of type ι → ι be given.

Assume H0: ∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∃ x2 . and (SNo x2) (∃ x3 . and (SNo x3) (∃ x4 . and (SNo x4) (∃ x5 . and (SNo x5) (∃ x6 . and (SNo x6) (∃ x7 . and (SNo x7) (∃ x8 . and (SNo x8) (x1 = bbc71.. (x0 x1) x2 x3 x4 x5 x6 x7 x8)))))))).

Assume H1: ∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1).

Let x1 of type ι → ι be given.

Assume H2: ∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∃ x3 . and (SNo x3) (∃ x4 . and (SNo x4) (∃ x5 . and (SNo x5) (∃ x6 . and (SNo x6) (∃ x7 . and (SNo x7) (∃ x8 . and (SNo x8) (x2 = bbc71.. (x0 x2) (x1 x2) x3 x4 x5 x6 x7 x8))))))).

Assume H3: ∀ x2 . 1eb0a.. x2 ⟶ SNo (x1 x2).

Let x2 of type ι → ι be given.

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

Assume H5: ∀ x3 . 1eb0a.. x3 ⟶ SNo (x2 x3).

Let x3 of type ι → ι be given.

Assume H6: ∀ x4 . 1eb0a.. x4 ⟶ and (SNo (x3 x4)) (∃ x5 . and (SNo x5) (∃ x6 . and (SNo x6) (∃ x7 . and (SNo x7) (∃ x8 . and (SNo x8) (x4 = bbc71.. (x0 x4) (x1 x4) (x2 x4) (x3 x4) x5 x6 x7 x8))))).

Let x4 of type ι be given.

Assume H7: 1eb0a.. x4.

Apply H6 with x4, and (SNo (41ec1.. x0 x1 x2 x3 x4)) (∃ x5 . and (SNo x5) (∃ x6 . and (SNo x6) (∃ x7 . and (SNo x7) (x4 = bbc71.. (x0 x4) (x1 x4) (x2 x4) (x3 x4) (41ec1.. x0 x1 x2 x3 x4) x5 x6 x7)))) leaving 2 subgoals.

The subproof is completed by applying H7.

Assume H8: SNo (x3 x4).

Assume H9: ∃ x5 . and (SNo x5) (∃ x6 . and (SNo x6) (∃ x7 . and (SNo x7) (∃ x8 . ...))).

...

■

Proofgold Proof