Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
be given.
Assume H0:
80242..
x0
.
Apply unknownprop_0b5b61a66a1ed2eb843dbce5c5f6930c63a284fe5e33704d9f0cc564310ec40b with
1216a..
(
4ae4a..
(
e4431..
x0
)
)
(
λ x1 .
(
λ x2 .
or
(
prim1
x2
x0
)
(
x2
=
e4431..
x0
)
)
x1
)
,
a4c2a..
(
4ae4a..
(
e4431..
x0
)
)
(
λ x1 .
not
(
(
λ x2 .
or
(
prim1
x2
x0
)
(
x2
=
e4431..
x0
)
)
x1
)
)
(
λ x1 .
(
λ x2 .
15418..
x2
(
91630..
(
4ae4a..
4a7ef..
)
)
)
x1
)
,
e4431..
x0
.
Apply unknownprop_1dada0fb38ff7f9b45b564ad11d6295d93250427446875218f17ee62431454a6 with
4ae4a..
(
e4431..
x0
)
,
λ x1 .
(
λ x2 .
or
(
prim1
x2
x0
)
(
x2
=
e4431..
x0
)
)
x1
,
e4431..
x0
leaving 2 subgoals.
The subproof is completed by applying unknownprop_38ce50d6b52a0a920b530e7796207ec902a42d65414467df1ecd3efb123f4cb9 with
e4431..
x0
.
Apply orIR with
prim1
(
e4431..
x0
)
x0
,
e4431..
x0
=
e4431..
x0
.
Let x1 of type
ι
→
ι
→
ο
be given.
Assume H1:
x1
(
e4431..
x0
)
(
e4431..
x0
)
.
The subproof is completed by applying H1.
■