Let x0 of type ι be given.

Assume H0: CSNo x0.

Apply Eps_i_ex with λ x1 . and (SNo x1) (x0 = SNo_pair (CSNo_Re x0) x1).

Apply CSNo_E with x0, λ x1 . ∃ x2 . and (SNo x2) (x1 = SNo_pair (CSNo_Re x1) x2) leaving 2 subgoals.

The subproof is completed by applying H0.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H1: SNo x1.

Assume H2: SNo x2.

Assume H3: x0 = SNo_pair x1 x2.

Let x3 of type ο be given.

Assume H4: ∀ x4 . and (SNo x4) (SNo_pair x1 x2 = SNo_pair (CSNo_Re (SNo_pair x1 x2)) x4) ⟶ x3.

Apply H4 with x2.

Apply andI with SNo x2, SNo_pair x1 x2 = SNo_pair (CSNo_Re (SNo_pair x1 x2)) x2 leaving 2 subgoals.

The subproof is completed by applying H2.

Apply CSNo_Re2 with x1, x2, λ x4 x5 . SNo_pair x1 x2 = SNo_pair x5 x2 leaving 3 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H2.

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

Assume H5: x4 (SNo_pair x1 x2) (SNo_pair x1 x2).

The subproof is completed by applying H5.

■

Proofgold Proof