Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: SNo x0.

Assume H1: SNo x1.

Let x2 of type ο be given.

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

Apply H2 with x0.

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

The subproof is completed by applying H0.

Let x3 of type ο be given.

Assume H3: ∀ x4 . and (SNo x4) (SNo_pair x0 x1 = SNo_pair x0 x4) ⟶ x3.

Apply H3 with x1.

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

The subproof is completed by applying H1.

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

Assume H4: x4 (SNo_pair x0 x1) (SNo_pair x0 x1).

The subproof is completed by applying H4.

■

Proofgold Proof