Proofgold Proof

pf

Let x0 of type ι be given.

Assume H0: Field x0.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H1: nIn x2 (K_field_0 x0 x0).

Claim L2: not (and (x1 ∈ K_field_0 x0 x0) (x2 ∈ setminus (K_field_0 x0 x0) (Sing (K_field_3 x0 x0))))

Assume H2: and (x1 ∈ K_field_0 x0 x0) (x2 ∈ setminus (K_field_0 x0 x0) (Sing (K_field_3 x0 x0))).

Apply H2 with False.

Assume H3: x1 ∈ K_field_0 x0 x0.

Assume H4: x2 ∈ setminus (K_field_0 x0 x0) (Sing (K_field_3 x0 x0)).

Apply setminusE with K_field_0 x0 x0, Sing (K_field_3 x0 x0), x2, False leaving 2 subgoals.

The subproof is completed by applying H4.

Assume H5: x2 ∈ K_field_0 x0 x0.

Assume H6: nIn x2 (Sing (K_field_3 x0 x0)).

Apply H1.

The subproof is completed by applying H5.

Apply If_i_0 with and (x1 ∈ K_field_0 x0 x0) (x2 ∈ setminus (K_field_0 x0 x0) (Sing (K_field_3 x0 x0))), prim0 (λ x3 . and (x3 ∈ K_field_0 x0 x0) (x1 = K_field_2_b x0 x0 x2 x3)), 0.

The subproof is completed by applying L2.

■