Let x0 of type ι be given.

Assume H0: 8c189.. x0.

Apply unknownprop_431ff8ff6435faa4c5f86e4f0a6c43deeb7869b72194a714b191972a3eaf6491 with x0, and (SNo (e5fe3.. x0)) (∃ x1 . and (SNo x1) (∃ x2 . and (SNo x2) (x0 = f4b0e.. (6b27d.. x0) (e5fe3.. x0) x1 x2))) leaving 2 subgoals.

The subproof is completed by applying H0.

Assume H1: SNo (6b27d.. x0).

Assume H2: ∃ x1 . and (SNo x1) (∃ x2 . and (SNo x2) (∃ x3 . and (SNo x3) (x0 = f4b0e.. (6b27d.. x0) x1 x2 x3))).

Apply Eps_i_ex with λ x1 . and (SNo x1) (∃ x2 . and (SNo x2) (∃ x3 . and (SNo x3) (x0 = f4b0e.. (6b27d.. x0) x1 x2 x3))).

The subproof is completed by applying H2.

■

Proofgold Proof