Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: nIn x0 x1.
Apply notE with In x0 x1.
Apply unknownprop_9bccc16873f624a3c3c071d170820d76e64a5491b15f0c2f0287b0026ecb19b8 with x0, x1.
The subproof is completed by applying H0.