Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
be given.
Assume H0:
In
x0
0
.
Apply FalseE with
∀ x1 .
In
x1
x0
⟶
∀ x2 .
In
x2
x1
⟶
∃ x3 .
∀ x4 .
(
ordinal
x3
⟶
and
(
exactly2
x3
)
(
not
(
exactly5
x4
)
)
)
⟶
(
(
ordinal
x3
⟶
exactly2
x3
)
⟶
atleast2
x3
⟶
(
(
not
(
atleast2
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
⟶
x3
=
x4
)
⟶
atleast3
x3
)
⟶
and
(
atleast5
x2
)
(
not
(
exactly1of2
(
SNoLt
x2
(
binrep
(
Power
(
Power
(
Power
(
Power
0
)
)
)
)
0
)
)
(
TransSet
x4
)
)
)
)
⟶
nat_p
x3
.
Apply unknownprop_1cc88f7e87aaf8c5cee24b4a69ff535a81e7855c45a9fd971eec05ee4cc28f9c with
x0
.
The subproof is completed by applying H0.
■