Search for blocks/addresses/...
Proofgold Term Root Disambiguation
∀ x0 .
∀ x1 x2 :
ι →
ι → ι
.
∀ x3 :
ι →
ι → ο
.
∀ x4 x5 .
unpack_b_b_r_e_e_o
(
pack_b_b_r_e_e
x0
x1
x2
x3
x4
x5
)
(
λ x7 .
λ x8 x9 :
ι →
ι → ι
.
λ x10 :
ι →
ι → ο
.
λ x11 x12 .
explicit_Reals
x7
x11
x12
x8
x9
x10
)
=
explicit_Reals
x0
x4
x5
x1
x2
x3
as obj
-
as prop
1e4af..
RealsStruct_unpack_eq
theory
HotG
stx
b2e5e..
address
TMKP2..
RealsStruct_unpack_eq