Search for blocks/addresses/...
Proofgold Term Root Disambiguation
λ x0 x1 .
∀ x2 : ο .
(
∀ x3 .
and
(
and
(
∀ x4 .
prim1
x4
x0
⟶
∀ x5 : ο .
(
∀ x6 .
and
(
prim1
x6
x1
)
(
prim1
(
7ee77..
x4
x6
)
x3
)
⟶
x5
)
⟶
x5
)
(
∀ x4 .
prim1
x4
x1
⟶
∀ x5 : ο .
(
∀ x6 .
and
(
prim1
x6
x0
)
(
prim1
(
7ee77..
x6
x4
)
x3
)
⟶
x5
)
⟶
x5
)
)
(
∀ x4 x5 x6 x7 .
prim1
(
7ee77..
x4
x5
)
x3
⟶
prim1
(
7ee77..
x6
x7
)
x3
⟶
iff
(
x4
=
x6
)
(
x5
=
x7
)
)
⟶
x2
)
⟶
x2
as obj
c2e41..
as prop
-
theory
HoTg
stx
f69d8..
address
TMQ55..