Search for blocks/addresses/...

Proofgold Proof

pf
Apply unknownprop_fa66e3d1737b2c05fa4008399b4c740ee88bf9334c6b435957b41684dfedfe51 with prim3 4a7ef...
Let x0 of type ι be given.
Assume H0: prim1 x0 (prim3 4a7ef..).
Apply UnionE with 4a7ef.., x0, False leaving 2 subgoals.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Assume H1: and (prim1 x0 x1) (prim1 x1 4a7ef..).
Apply unknownprop_da3368fefc81e401e6446c98c0c04ab87d76d6f97c47fe5fd07c1e3c2f00ef6a with x1.
Apply andER with prim1 x0 x1, prim1 x1 4a7ef...
The subproof is completed by applying H1.
■