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

Let x1 of type ι be given.

Assume H1: 1eb0a.. x1.

Apply unknownprop_35aad255a0ebc1a79b9cd24e9634a038476cfcc2bcb07410ad3e7bec2e8f5a27 with x0, x1, SNo (d4639.. x0 x1) leaving 3 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

Assume H2: SNo (d4639.. x0 x1).

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

The subproof is completed by applying H2.

■

Proofgold Proof