Search for blocks/addresses/...
Proofgold Term Root Disambiguation
λ x0 x1 x2 .
unpack_c_o
x0
(
λ x3 .
λ x4 :
(
ι → ο
)
→ ο
.
unpack_c_o
x1
(
λ x5 .
λ x6 :
(
ι → ο
)
→ ο
.
and
(
x2
∈
setexp
x5
x3
)
(
∀ x7 :
ι → ο
.
(
∀ x8 .
x7
x8
⟶
x8
∈
x5
)
⟶
x6
x7
⟶
x4
(
λ x8 .
and
(
x8
∈
x3
)
(
x7
(
ap
x2
x8
)
)
)
)
)
)
as obj
4ebd3..
Hom_struct_c
as prop
-
theory
HotG
stx
820be..
address
TMHam..
Hom_struct_c