Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
be given.
Assume H0:
f4ccf..
x0
.
Apply H0 with
λ x1 .
x1
=
c0301..
(
f482f..
x1
4a7ef..
)
(
f482f..
(
f482f..
x1
(
4ae4a..
4a7ef..
)
)
)
.
Let x1 of type
ι
be given.
Let x2 of type
ι
→
ι
be given.
Assume H1:
∀ x3 .
prim1
x3
x1
⟶
prim1
(
x2
x3
)
x1
.
Apply unknownprop_64b30c93b63a275b33e0b1e088688090a219594d60d94e87e633646df8931180 with
x1
,
x2
,
λ x3 x4 .
c0301..
x1
x2
=
c0301..
x3
(
f482f..
(
f482f..
(
c0301..
x1
x2
)
(
4ae4a..
4a7ef..
)
)
)
.
Apply unknownprop_d27ca5a7814f2daf5c8c6eeb959eb2a9b63bbdb9f85bbcbfe3480db840462db0 with
x1
,
x2
,
f482f..
(
f482f..
(
c0301..
x1
x2
)
(
4ae4a..
4a7ef..
)
)
.
The subproof is completed by applying unknownprop_f58b95d170c532b1a6ac682a4e91de3a8560ab9616f3c2e2f8b45045ae40523f with
x1
,
x2
.
■