Let x0 of type ι be given.

Assume H0: x0 ∈ complex.

Apply complex_E with x0, CSNo x0 leaving 2 subgoals.

The subproof is completed by applying H0.

Let x1 of type ι be given.

Assume H1: x1 ∈ real.

Let x2 of type ι be given.

Assume H2: x2 ∈ real.

Assume H3: x0 = SNo_pair x1 x2.

Apply H3 with λ x3 x4 . CSNo x4.

Apply CSNo_I with x1, x2 leaving 2 subgoals.

Apply real_SNo with x1.

The subproof is completed by applying H1.

Apply real_SNo with x2.

The subproof is completed by applying H2.

■

Proofgold Proof