Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
be given.
The subproof is completed by applying Sep_Subq with
SNoS_
(
SNoLev
x0
)
,
λ x1 .
SNoLt
x0
x1
.
■