Search for blocks/addresses/...
Proofgold Proof
pf
The subproof is completed by applying binunionI1 with
omega
,
{
minus_SNo
x0
|x0 ∈
omega
}
.
■