Search for blocks/addresses/...
Proofgold Proof
pf
Apply SNoL_0 with
λ x0 x1 .
{x2 ∈
x1
|
SNoLe
0
x2
}
=
0
.
The subproof is completed by applying Sep_Empty with
λ x0 .
SNoLe
0
x0
.
■