Let x0 of type ι be given.

Assume H0: CSNo x0.

Let x1 of type ι → ο be given.

Assume H1: ∀ x2 x3 . SNo x2 ⟶ SNo x3 ⟶ x0 = SNo_pair x2 x3 ⟶ x1 (SNo_pair x2 x3).

Apply H0 with x1 x0.

Let x2 of type ι be given.

Assume H2: (λ x3 . and (SNo x3) (∃ x4 . and (SNo x4) (x0 = SNo_pair x3 x4))) x2.

Apply H2 with x1 x0.

Assume H3: SNo x2.

Assume H4: ∃ x3 . and (SNo x3) (x0 = SNo_pair x2 x3).

Apply H4 with x1 x0.

Let x3 of type ι be given.

Assume H5: (λ x4 . and (SNo x4) (x0 = SNo_pair x2 x4)) x3.

Apply H5 with x1 x0.

Assume H6: SNo x3.

Assume H7: x0 = SNo_pair x2 x3.

Apply H7 with λ x4 x5 . x1 x5.

Apply H1 with x2, x3 leaving 3 subgoals.

The subproof is completed by applying H3.

The subproof is completed by applying H6.

The subproof is completed by applying H7.

■

Proofgold Proof