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))))).

Assume H7: ∀ x4 . 1eb0a.. x4 ⟶ SNo (x3 x4).

Let x4 of type ι → ι be given.

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

Let x5 of type ι be given.

Assume H9: 1eb0a.. x5.

Apply H8 with x5, and (SNo (28f5a.. x0 x1 x2 x3 x4 x5)) (∃ x6 . and (SNo x6) ...) leaving 2 subgoals.

...

■

Proofgold Proof