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 (field0 x0).

Claim L2: not (and (x1 ∈ field0 x0) (x2 ∈ setminus (field0 x0) (Sing (field3 x0))))

Assume H2: and (x1 ∈ field0 x0) (x2 ∈ setminus (field0 x0) (Sing (field3 x0))).

Apply H2 with False.

Assume H3: x1 ∈ field0 x0.

Assume H4: x2 ∈ setminus (field0 x0) (Sing (field3 x0)).

Apply setminusE with field0 x0, Sing (field3 x0), x2, False leaving 2 subgoals.

The subproof is completed by applying H4.

Assume H5: x2 ∈ field0 x0.

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

Apply H1.

The subproof is completed by applying H5.

Apply If_i_0 with and (x1 ∈ field0 x0) (x2 ∈ setminus (field0 x0) (Sing (field3 x0))), prim0 (λ x3 . and (x3 ∈ field0 x0) (x1 = field2b x0 x2 x3)), 0.

The subproof is completed by applying L2.

■