Search for blocks/addresses/...
Proofgold Proof
pf
Assume H0:
∀ x0 .
∀ x1 : ο .
SNo
x0
⟶
ordinal
(
SNoLev
x0
)
⟶
x1
.
Claim L1:
SNo
0
The subproof is completed by applying SNo_0.
Claim L2:
not
(
ordinal
(
SNoLev
0
)
⟶
False
)
Apply SNoLev_0 with
λ x0 x1 .
not
(
ordinal
x1
⟶
False
)
.
Assume H2:
ordinal
0
⟶
False
.
Apply H2.
The subproof is completed by applying ordinal_Empty.
Apply L2.
Apply H0 with
0
,
False
.
The subproof is completed by applying L1.
■