Search for blocks/addresses/...

Proofgold Term Root Disambiguation

λ x0 . and (struct_b_b_r_e_e x0) (unpack_b_b_r_e_e_o x0 (λ x1 . λ x2 x3 : ι → ι → ι . λ x4 : ι → ι → ο . λ x5 x6 . explicit_Reals x1 x5 x6 x2 x3 x4))
as obj
3d1a7..RealsStruct
as prop
-
theory
HotG
stx
b2e5e..
address
TMJjj..RealsStruct