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.

Let x5 of type ι be given.

Let x6 of type ι be given.

Let x7 of type ι be given.

Let x8 of type ι be given.

Let x9 of type ι be given.

Let x10 of type ι be given.

Let x11 of type ι be given.

Assume H8: SNo x4.

Assume H9: SNo x5.

Assume H10: SNo x6.

Assume H11: SNo x7.

Assume H12: SNo x8.

Assume H13: SNo x9.

Assume H14: SNo x10.

Assume H15: SNo x11.

Apply unknownprop_6885b34a909c57357a9371c8f632d305bcfee5a7dda52ca2bf191272f9ad5d31 with x0, x1, x2, x3, bbc71.. x4 x5 x6 x7 x8 x9 x10 x11, 41ec1.. x0 x1 x2 x3 (bbc71.. x4 x5 x6 x7 x8 x9 x10 x11) = x8 leaving 9 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.

...

■

Proofgold Proof