Let x0 of type ι be given.

Assume H0: c7ce4.. x0.

Apply H0 with 8c189.. x0.

Let x1 of type ι be given.

Assume H1: (λ x2 . and (SNo x2) (∃ x3 . and (SNo x3) (x0 = ad280.. x2 x3))) x1.

Apply H1 with 8c189.. x0.

Assume H2: SNo x1.

Assume H3: ∃ x2 . and (SNo x2) (x0 = ad280.. x1 x2).

Apply H3 with 8c189.. x0.

Let x2 of type ι be given.

Assume H4: (λ x3 . and (SNo x3) (x0 = ad280.. x1 x3)) x2.

Apply H4 with 8c189.. x0.

Assume H5: SNo x2.

Assume H6: x0 = ad280.. x1 x2.

Let x3 of type ο be given.

Assume H7: ∀ x4 . and (SNo x4) (∃ x5 . and (SNo x5) (∃ x6 . and (SNo x6) (∃ x7 . and (SNo x7) (x0 = f4b0e.. x4 x5 x6 x7)))) ⟶ x3.

Apply H7 with x1.

Apply andI with SNo x1, ∃ x4 . and (SNo x4) (∃ x5 . and (SNo x5) (∃ x6 . and (SNo x6) (x0 = f4b0e.. x1 x4 x5 x6))) leaving 2 subgoals.

The subproof is completed by applying H2.

Let x4 of type ο be given.

Assume H8: ∀ x5 . and (SNo x5) (∃ x6 . and (SNo x6) (∃ x7 . and (SNo x7) (x0 = f4b0e.. x1 x5 x6 x7))) ⟶ x4.

Apply H8 with x2.

Apply andI with SNo x2, ∃ x5 . and (SNo x5) (∃ x6 . and (SNo x6) (x0 = f4b0e.. x1 x2 x5 x6)) leaving 2 subgoals.

The subproof is completed by applying H5.

Let x5 of type ο be given.

Assume H9: ∀ x6 . and (SNo x6) (∃ x7 . and (SNo x7) (x0 = f4b0e.. x1 x2 x6 x7)) ⟶ x5.

Apply H9 with 0.

Apply andI with SNo 0, ∃ x6 . and (SNo x6) (x0 = f4b0e.. x1 x2 0 x6) leaving 2 subgoals.

The subproof is completed by applying SNo_0.

Let x6 of type ο be given.

Assume H10: ∀ x7 . and (SNo x7) (x0 = f4b0e.. x1 x2 0 x7) ⟶ x6.

Apply H10 with 0.

Apply andI with SNo 0, x0 = f4b0e.. x1 x2 0 0 leaving 2 subgoals.

The subproof is completed by applying SNo_0.

Apply unknownprop_af847e040e91b99dbf77a9d137cb8611c75d491ea2b42e1ae03082b87361b50c with x1, x2, λ x7 x8 . x0 = x8.

The subproof is completed by applying H6.

■

Proofgold Proof