Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
be given.
Let x1 of type
ι
be given.
Apply unknownprop_34a9c3ddf8f86ff1fd1503067affdc551cb9b84b389e43c3ef15ff484c15f415 with
x0
,
x1
,
prim1
x1
(
e5b72..
x0
)
⟶
Subq
x1
x0
.
Assume H0:
prim1
x1
(
e5b72..
x0
)
⟶
Subq
x1
x0
.
Assume H1:
Subq
x1
x0
⟶
prim1
x1
(
e5b72..
x0
)
.
The subproof is completed by applying H0.
■