Search for blocks/addresses/...
Proofgold Proof
pf
Apply set_ext with
e5b72..
4a7ef..
,
91630..
4a7ef..
leaving 2 subgoals.
Let x0 of type
ι
be given.
Assume H0:
prim1
x0
(
e5b72..
4a7ef..
)
.
Claim L1:
x0
=
4a7ef..
Apply unknownprop_ea78574cb3264467ecb0cee6dab0f2cbbdf0e0a00f843238d57e1be6acdbe25f with
x0
.
Apply unknownprop_4134b8a5d866cd7ad711ea569ada0ca0ba949f5cad571bf5782dc7c2d15cdb1c with
4a7ef..
,
x0
.
The subproof is completed by applying H0.
Apply L1 with
λ x1 x2 .
prim1
x2
(
91630..
4a7ef..
)
.
The subproof is completed by applying unknownprop_c6d721b795faf1c324094ad380dfe62a3a5dc2ef0b2edf42237be188f6768728 with
4a7ef..
.
Let x0 of type
ι
be given.
Assume H0:
prim1
x0
(
91630..
4a7ef..
)
.
Apply unknownprop_30833a9978e304b25ffd59c347245315985872140acc9e441a97543a28184d79 with
4a7ef..
,
x0
,
λ x1 x2 .
prim1
x2
(
e5b72..
4a7ef..
)
leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_21eccfc5b947b8f10314dfc0734b94272c3a79b52ca9a3c84823212c3425dcb8 with
4a7ef..
.
■