Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
be given.
Assume H0:
ordinal
(
(
λ x1 .
15418..
x1
(
91630..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x0
)
.
Claim L1:
prim1
(
91630..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
(
(
λ x1 .
15418..
x1
(
91630..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x0
)
Apply unknownprop_e4d6e0bfb4ef6d52ee13edd54a77c8cc7f0a3af8ffb1b8da66d4f98842dd28b5 with
x0
,
91630..
(
91630..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
,
91630..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
.
The subproof is completed by applying unknownprop_c6d721b795faf1c324094ad380dfe62a3a5dc2ef0b2edf42237be188f6768728 with
91630..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
.
Apply unknownprop_233a01ed74afb32f65afd3e8784abd0a97273e5d2c2787b08adfb08e640439ec.
Apply ordinal_Hered with
(
λ x1 .
15418..
x1
(
91630..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x0
,
91630..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L1.
■