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.
■