Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Let x3 of type ι be given.

Assume H0: SNo x0.

Assume H1: SNo x1.

Assume H2: SNo x2.

Assume H3: SNo x3.

Apply unknownprop_431ff8ff6435faa4c5f86e4f0a6c43deeb7869b72194a714b191972a3eaf6491 with f4b0e.. x0 x1 x2 x3, 6b27d.. (f4b0e.. x0 x1 x2 x3) = x0 leaving 2 subgoals.

Apply unknownprop_1c4b77a1bdf71ac8c46772d8b01bd6609e54ee74070e16498c4800adfe13c5ca with x0, x1, x2, x3 leaving 4 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 (6b27d.. (f4b0e.. x0 x1 x2 x3)).

Assume H5: ∃ x4 . and (SNo x4) (∃ x5 . and (SNo x5) (∃ x6 . and (SNo x6) (f4b0e.. x0 x1 x2 x3 = f4b0e.. (6b27d.. (f4b0e.. x0 x1 x2 x3)) x4 x5 x6))).

Apply H5 with 6b27d.. (f4b0e.. x0 x1 x2 x3) = x0.

Let x4 of type ι be given.

Assume H6: (λ x5 . and (SNo x5) (∃ x6 . and (SNo x6) (∃ x7 . and (SNo x7) (f4b0e.. x0 x1 x2 x3 = f4b0e.. (6b27d.. (f4b0e.. x0 x1 x2 x3)) x5 x6 x7)))) x4.

Apply H6 with 6b27d.. (f4b0e.. x0 x1 x2 x3) = x0.

Assume H7: SNo x4.

Assume H8: ∃ x5 . and (SNo x5) (∃ x6 . and (SNo x6) (f4b0e.. x0 x1 x2 x3 = f4b0e.. (6b27d.. (f4b0e.. x0 x1 x2 x3)) x4 x5 x6)).

Apply H8 with 6b27d.. (f4b0e.. x0 x1 x2 x3) = x0.

Let x5 of type ι be given.

Assume H9: (λ x6 . and (SNo x6) (∃ x7 . and (SNo x7) (f4b0e.. x0 x1 x2 x3 = f4b0e.. (6b27d.. (f4b0e.. x0 x1 x2 x3)) x4 x6 x7))) x5.

Apply H9 with 6b27d.. (f4b0e.. x0 x1 x2 x3) = x0.

Assume H10: SNo x5.

Assume H11: ∃ x6 . and (SNo x6) (f4b0e.. x0 x1 x2 x3 = f4b0e.. (6b27d.. (f4b0e.. x0 x1 x2 x3)) x4 x5 x6).

Apply H11 with 6b27d.. (f4b0e.. x0 x1 x2 x3) = x0.

Let x6 of type ι be given.

Assume H12: (λ x7 . and (SNo x7) (f4b0e.. x0 x1 x2 x3 = f4b0e.. (6b27d.. (f4b0e.. x0 x1 x2 x3)) x4 x5 x7)) x6.

Apply H12 with 6b27d.. (f4b0e.. x0 x1 x2 x3) = x0.

Assume H13: SNo x6.

Assume H14: f4b0e.. x0 x1 x2 x3 = f4b0e.. (6b27d.. (f4b0e.. x0 x1 x2 x3)) ... ... ....

...

■

Proofgold Proof