Search for blocks/addresses/...

Proofgold Proof

pf
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 (x3x0) (and (and (PNoEq_ x3 x1 x1) (not (x1 x3))) (x1 x3))) x2.
Apply H1 with False.
Assume H2: x2x0.
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 x2False.
Assume H5: PNoEq_ x2 x1 x1.
Assume H6: not (x1 x2).
Assume H7: x1 x2.
Apply H6.
The subproof is completed by applying H7.