Search for blocks/addresses/...
Proofgold Term Root Disambiguation
λ x0 x1 .
19c2c..
x1
(
λ x2 .
λ x3 :
ι →
ι → ι
.
1216a..
48ef8..
(
λ x4 .
∀ x5 : ο .
(
∀ x6 .
and
(
prim1
x6
(
b5c9f..
x2
(
4ae4a..
x4
)
)
)
(
∀ x7 .
prim1
x7
(
4ae4a..
x4
)
⟶
∀ x8 .
prim1
x8
(
4ae4a..
x4
)
⟶
(
x7
=
x8
⟶
∀ x9 : ο .
x9
)
⟶
∀ x9 .
prim1
x9
(
f482f..
x0
4a7ef..
)
⟶
∀ x10 .
prim1
x10
(
f482f..
x0
4a7ef..
)
⟶
x3
(
f482f..
x6
x7
)
x9
=
x3
(
f482f..
x6
x8
)
x10
⟶
∀ x11 : ο .
x11
)
⟶
x5
)
⟶
x5
)
)
as obj
95464..
as prop
-
theory
HoTg
stx
4b82f..
address
TMbZo..