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

Let x2 of type ι be given.

Assume H3: 1eb0a.. x2.

Apply unknownprop_959771339f7cf71f620f34cfd369621e1910f352584f3a6002a869b8d17cee3a with x0, x1, x2, SNo (50208.. x0 x1 x2) leaving 5 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.

Assume H4: SNo (50208.. x0 x1 x2).

Assume H5: ∃ x3 . and (SNo x3) (∃ x4 . and (SNo x4) (∃ x5 . and (SNo x5) (∃ x6 . and (SNo x6) (∃ x7 . and (SNo x7) (x2 = bbc71.. (x0 x2) (x1 x2) (50208.. x0 x1 x2) x3 x4 x5 x6 x7))))).

The subproof is completed by applying H4.

■

Proofgold Proof