Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
be given.
Let x1 of type
ι
be given.
Assume H0:
80242..
x0
.
Assume H1:
80242..
x1
.
Apply unknownprop_b7caf5f70ae79c72282a4433b7742206b9e82c71b0701b7f8019ceccbdfb80a7 with
x0
,
x1
,
02b90..
(
0ac37..
(
94f9e..
(
23e07..
x0
)
(
λ x2 .
bc82c..
x2
x1
)
)
(
94f9e..
(
23e07..
x1
)
(
λ x2 .
bc82c..
x0
x2
)
)
)
(
0ac37..
(
94f9e..
(
5246e..
x0
)
(
λ x2 .
bc82c..
x2
x1
)
)
(
94f9e..
(
5246e..
x1
)
(
λ x2 .
bc82c..
x0
x2
)
)
)
leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Assume H2:
and
(
and
(
and
(
and
(
80242..
(
bc82c..
x0
x1
)
)
(
∀ x2 .
prim1
x2
(
23e07..
x0
)
⟶
099f3..
(
bc82c..
x2
x1
)
(
bc82c..
x0
x1
)
)
)
(
∀ x2 .
prim1
x2
(
5246e..
x0
)
⟶
099f3..
(
bc82c..
x0
x1
)
(
bc82c..
x2
x1
)
)
)
(
∀ x2 .
prim1
x2
(
23e07..
x1
)
⟶
099f3..
(
bc82c..
x0
x2
)
(
bc82c..
x0
x1
)
)
)
(
∀ x2 .
prim1
x2
(
5246e..
x1
)
⟶
099f3..
(
bc82c..
x0
x1
)
(
bc82c..
x0
x2
)
)
.
Assume H3:
02b90..
(
0ac37..
(
94f9e..
(
23e07..
x0
)
(
λ x2 .
bc82c..
x2
x1
)
)
(
94f9e..
(
23e07..
x1
)
(
bc82c..
x0
)
)
)
(
0ac37..
(
94f9e..
(
5246e..
x0
)
(
λ x2 .
bc82c..
x2
x1
)
)
(
94f9e..
(
5246e..
x1
)
(
bc82c..
x0
)
)
)
.
The subproof is completed by applying H3.
■