Search for blocks/addresses/...
Proofgold Term Root Disambiguation
λ x0 x1 .
09072..
(
7b9f3..
(
λ x2 .
λ x3 :
ι → ο
.
and
(
ordinal
x2
)
(
prim1
(
09072..
x2
x3
)
x0
)
)
(
λ x2 .
λ x3 :
ι → ο
.
and
(
ordinal
x2
)
(
prim1
(
09072..
x2
x3
)
x1
)
)
)
(
ce2d5..
(
λ x2 .
λ x3 :
ι → ο
.
and
(
ordinal
x2
)
(
prim1
(
09072..
x2
x3
)
x0
)
)
(
λ x2 .
λ x3 :
ι → ο
.
and
(
ordinal
x2
)
(
prim1
(
09072..
x2
x3
)
x1
)
)
)
as obj
02a50..
as prop
-
theory
HoTg
stx
38a69..
address
TMMKk..