Search for blocks/addresses/...
Proofgold Proof
pf
Apply unknownprop_f04ee3f2db7dade92ee7be101bff40fb89f733bb0c0340f09b616cd72154ad93 with
λ x0 .
(
λ x1 .
∀ x2 .
80242..
x2
⟶
∀ x3 : ο .
(
80242..
(
e6316..
x1
x2
)
⟶
(
∀ x4 .
prim1
x4
(
23e07..
x1
)
⟶
∀ x5 .
prim1
x5
(
23e07..
x2
)
⟶
099f3..
(
bc82c..
(
e6316..
x4
x2
)
(
e6316..
x1
x5
)
)
(
bc82c..
(
e6316..
x1
x2
)
(
e6316..
x4
x5
)
)
)
⟶
(
∀ x4 .
prim1
x4
(
5246e..
x1
)
⟶
∀ x5 .
prim1
x5
(
5246e..
x2
)
⟶
099f3..
(
bc82c..
(
e6316..
x4
x2
)
(
e6316..
x1
x5
)
)
(
bc82c..
(
e6316..
x1
x2
)
(
e6316..
x4
x5
)
)
)
⟶
(
∀ x4 .
prim1
x4
(
23e07..
x1
)
⟶
∀ x5 .
prim1
x5
(
5246e..
x2
)
⟶
099f3..
(
bc82c..
(
e6316..
x1
x2
)
(
e6316..
x4
x5
)
)
(
bc82c..
(
e6316..
x4
x2
)
(
e6316..
x1
x5
)
)
)
⟶
(
∀ x4 .
prim1
x4
(
5246e..
x1
)
⟶
∀ x5 .
prim1
x5
(
23e07..
x2
)
⟶
099f3..
(
bc82c..
(
e6316..
x1
x2
)
(
e6316..
x4
x5
)
)
(
bc82c..
(
e6316..
x4
x2
)
(
e6316..
x1
x5
)
)
)
⟶
x3
)
⟶
x3
)
x0
.
Let x0 of type
ι
be given.
Assume H0:
80242..
x0
.
Assume H1:
∀ x1 .
prim1
x1
(
56ded..
(
e4431..
x0
)
)
⟶
(
λ x2 .
∀ x3 .
80242..
x3
⟶
∀ x4 : ο .
(
80242..
(
e6316..
x2
x3
)
⟶
(
∀ x5 .
prim1
x5
(
23e07..
x2
)
⟶
∀ x6 .
prim1
x6
(
23e07..
x3
)
⟶
099f3..
(
bc82c..
(
e6316..
x5
x3
)
(
e6316..
x2
x6
)
)
(
bc82c..
(
e6316..
x2
x3
)
(
e6316..
x5
x6
)
)
)
⟶
(
∀ x5 .
prim1
x5
(
5246e..
x2
)
⟶
∀ x6 .
prim1
x6
(
5246e..
x3
)
⟶
099f3..
(
bc82c..
(
e6316..
x5
x3
)
(
e6316..
x2
x6
)
)
(
bc82c..
(
e6316..
x2
x3
)
(
e6316..
x5
x6
)
)
)
⟶
(
∀ x5 .
prim1
x5
(
23e07..
x2
)
⟶
∀ x6 .
prim1
x6
(
5246e..
x3
)
⟶
099f3..
(
bc82c..
(
e6316..
x2
x3
)
(
e6316..
x5
x6
)
)
(
bc82c..
(
e6316..
x5
x3
)
(
e6316..
x2
x6
)
)
)
⟶
(
∀ x5 .
prim1
x5
(
5246e..
x2
)
⟶
∀ x6 .
prim1
x6
(
23e07..
x3
)
⟶
099f3..
(
bc82c..
(
e6316..
x2
x3
)
(
e6316..
x5
x6
)
)
(
bc82c..
(
e6316..
x5
x3
)
(
e6316..
x2
x6
)
)
)
⟶
x4
)
⟶
x4
)
x1
.
Apply unknownprop_f04ee3f2db7dade92ee7be101bff40fb89f733bb0c0340f09b616cd72154ad93 with
λ x1 .
(
λ x2 .
∀ x3 : ο .
(
...
⟶
...
⟶
...
⟶
...
⟶
(
∀ x4 .
...
⟶
∀ x5 .
...
⟶
099f3..
(
bc82c..
(
e6316..
x0
x2
)
(
e6316..
x4
x5
)
)
(
bc82c..
(
e6316..
x4
...
)
...
)
)
⟶
x3
)
⟶
x3
)
...
.
...
■