Let x0 of type ι be given.

Assume H0: SNo x0.

Let x1 of type ο be given.

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

Apply H1 with x0.

Apply andI with SNo x0, ∃ x2 . and (SNo x2) (x0 = SNo_pair x0 x2) leaving 2 subgoals.

The subproof is completed by applying H0.

Let x2 of type ο be given.

Assume H2: ∀ x3 . and (SNo x3) (x0 = SNo_pair x0 x3) ⟶ x2.

Apply H2 with 0.

Apply andI with SNo 0, x0 = SNo_pair x0 0 leaving 2 subgoals.

The subproof is completed by applying SNo_0.

Let x3 of type ι → ι → ο be given.

The subproof is completed by applying SNo_pair_0 with x0, λ x4 x5 . x3 x5 x4.

■

Proofgold Proof