Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
be given.
Assume H0:
30750..
x0
.
Apply H0 with
λ x1 .
x1
=
987b2..
(
f482f..
x1
4a7ef..
)
(
e3162..
(
f482f..
x1
(
4ae4a..
4a7ef..
)
)
)
.
Let x1 of type
ι
be given.
Let x2 of type
ι
→
ι
→
ι
be given.
Assume H1:
∀ x3 .
prim1
x3
x1
⟶
∀ x4 .
prim1
x4
x1
⟶
prim1
(
x2
x3
x4
)
x1
.
Apply unknownprop_8674365f14b0285b3312b4875395e693d6df9b10fe9756f39519b30aacbeca91 with
x1
,
x2
,
λ x3 x4 .
987b2..
x1
x2
=
987b2..
x3
(
e3162..
(
f482f..
(
987b2..
x1
x2
)
(
4ae4a..
4a7ef..
)
)
)
.
Apply unknownprop_d45876018bd1c8a04fed4c22e23277ef3c518489a1fd1bb4edfb07f8fb3466d0 with
x1
,
x2
,
e3162..
(
f482f..
(
987b2..
x1
x2
)
(
4ae4a..
4a7ef..
)
)
.
The subproof is completed by applying unknownprop_a59155e51c734938987e2b9ffb79da15884213566add9a57beb57783508c1eb2 with
x1
,
x2
.
■