Let x0 of type ι be given.

Let x1 of type ι → ο be given.

Assume H0: PNoLt_ x0 x1 x1.

Apply H0 with False.

Let x2 of type ι be given.

Assume H1: (λ x3 . and (prim1 x3 x0) (and (and (PNoEq_ x3 x1 x1) (not (x1 x3))) (x1 x3))) x2.

Apply H1 with False.

Assume H2: prim1 x2 x0.

Assume H3: and (and (PNoEq_ x2 x1 x1) (not (x1 x2))) (x1 x2).

Apply H3 with False.

Assume H4: and (PNoEq_ x2 x1 x1) (not (x1 x2)).

Apply H4 with x1 x2 ⟶ False.

Assume H5: PNoEq_ x2 x1 x1.

Assume H6: not (x1 x2).

Assume H7: x1 x2.

Apply H6.

The subproof is completed by applying H7.

■

Proofgold Proof