Search for blocks/addresses/...
Proofgold Proof
pf
Apply functional extensionality with
aae7a..
,
λ x0 x1 .
0fc90..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
(
λ x2 .
If_i
(
x2
=
4a7ef..
)
x0
x1
)
.
Let x0 of type
ι
be given.
Apply functional extensionality with
aae7a..
x0
,
(
λ x1 x2 .
0fc90..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
(
λ x3 .
If_i
(
x3
=
4a7ef..
)
x1
x2
)
)
x0
.
Let x1 of type
ι
be given.
The subproof is completed by applying unknownprop_dc63f07f5e92258921347b0c89ef1b6f68ff3d0c7d527390f78d57fc4bdb18d0 with
x0
,
x1
.
■