Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Apply set_ext with 0ac37.. 4a7ef.. x0, x0 leaving 2 subgoals.
Let x1 of type ι be given.
Assume H0: prim1 x1 (0ac37.. 4a7ef.. x0).
Apply unknownprop_b46721c187c37140cbae22d356b00ba89f4126d81d8665e4be15b5a58c78d06f with 4a7ef.., x0, x1, prim1 x1 x0 leaving 3 subgoals.
The subproof is completed by applying H0.
Assume H1: prim1 x1 4a7ef...
Apply FalseE with prim1 x1 x0.
Apply unknownprop_da3368fefc81e401e6446c98c0c04ab87d76d6f97c47fe5fd07c1e3c2f00ef6a with x1.
The subproof is completed by applying H1.
Assume H1: prim1 x1 x0.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Assume H0: prim1 x1 x0.
Apply unknownprop_e4d6e0bfb4ef6d52ee13edd54a77c8cc7f0a3af8ffb1b8da66d4f98842dd28b5 with 4a7ef.., x0, x1.
The subproof is completed by applying H0.