Search for blocks/addresses/...
Proofgold Term Root Disambiguation
∀ x0 :
ι → ο
.
x0
1
⟶
∀ x1 : ο .
(
∀ x2 .
(
∀ x3 : ο .
(
∀ x4 :
ι → ι
.
MetaCat_terminal_p
x0
HomSet
(
λ x5 .
lam
x5
(
λ x6 .
x6
)
)
(
λ x5 x6 x7 x8 x9 .
lam
x5
(
λ x10 .
ap
x8
(
ap
x9
x10
)
)
)
x2
x4
⟶
x3
)
⟶
x3
)
⟶
x1
)
⟶
x1
as obj
-
as prop
4cd1b..
MetaCatSet_terminal_gen
theory
HotG
stx
2772d..
address
TMXCP..
MetaCatSet_terminal_gen