Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H0: nIn x2 (binunion x0 x1).
Apply andE with nIn x2 x0, nIn x2 x1.
Apply unknownprop_2882b5d61fd4bb8b4472fe7a225676cd56469345a547230c02751aef67d3690b with x0, x1, x2.
The subproof is completed by applying H0.