Search for blocks/addresses/...

Proofgold Proof

pf
Apply andI with TransSet 4a7ef.., ∀ x0 . prim1 x0 4a7ef..TransSet x0 leaving 2 subgoals.
Let x0 of type ι be given.
Assume H0: prim1 x0 4a7ef...
Apply FalseE with Subq x0 4a7ef...
Apply unknownprop_da3368fefc81e401e6446c98c0c04ab87d76d6f97c47fe5fd07c1e3c2f00ef6a with x0.
The subproof is completed by applying H0.
Let x0 of type ι be given.
Assume H0: prim1 x0 4a7ef...
Apply FalseE with TransSet x0.
Apply unknownprop_da3368fefc81e401e6446c98c0c04ab87d76d6f97c47fe5fd07c1e3c2f00ef6a with x0.
The subproof is completed by applying H0.