Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: CSNo x0.

Assume H1: CSNo x1.

Assume H2: CSNo_Re x0 = CSNo_Re x1.

Assume H3: CSNo_Im x0 = CSNo_Im x1.

set y2 to be x0

set y3 to be y2

Claim L4: ∀ x4 : ι → ο . x4 y3 ⟶ x4 y2

Let x4 of type ι → ο be given.

Assume H4: x4 y3.

Apply CSNo_ReIm with y2, λ x5 . x4 leaving 2 subgoals.

The subproof is completed by applying H0.

set y5 to be SNo_pair (CSNo_Re y2) (CSNo_Im y2)

set y6 to be x4

Claim L5: ∀ x7 : ι → ο . x7 y6 ⟶ x7 y5

Let x7 of type ι → ο be given.

Assume H5: x7 y5.

Apply H2 with λ x8 x9 . SNo_pair x9 (CSNo_Im x4) = SNo_pair (CSNo_Re y5) (CSNo_Im y5), λ x8 . x7 leaving 2 subgoals.

Apply H3 with λ x8 x9 . SNo_pair (CSNo_Re y5) x9 = SNo_pair (CSNo_Re y5) (CSNo_Im y5).

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

The subproof is completed by applying H6.

set y8 to be λ x8 . x7

Apply CSNo_ReIm with y5, λ x9 x10 . y8 x10 x9 leaving 2 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H5.

set y7 to be λ x7 . y6

Apply L5 with λ x8 . y7 x8 y6 ⟶ y7 y6 x8 leaving 2 subgoals.

Assume H6: y7 y6 y6.

The subproof is completed by applying H6.

The subproof is completed by applying L5.

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

Apply L4 with λ x5 . x4 x5 y3 ⟶ x4 y3 x5.

Assume H5: x4 y3 y3.

The subproof is completed by applying H5.

■

Proofgold Proof