Search for blocks/addresses/...
Proofgold Term Root Disambiguation
λ x0 x1 .
λ x2 :
ι → ι
.
λ x3 .
λ x4 :
ι →
ι → ι
.
λ x5 x6 .
∀ x7 :
ι →
ι → ο
.
x7
x1
x3
⟶
(
∀ x8 .
prim1
x8
x0
⟶
∀ x9 .
x7
x8
x9
⟶
x7
(
x2
x8
)
(
x4
x8
x9
)
)
⟶
x7
x5
x6
as obj
a813b..
as prop
-
theory
HoTg
stx
ddc14..
address
TMSGx..