Search for blocks/addresses/...
Proofgold Term Root Disambiguation
∃ x0 x2 x4 :
ι →
ι → ι
.
∃ x6 :
ι →
ι →
ι →
ι →
ι → ι
.
MetaCat_product_constr_p
struct_p
UnaryPredHom
struct_id
struct_comp
x0
x2
x4
x6
as obj
-
as prop
4f9ac..
MetaCat_struct_p_product_constr
theory
HotG
stx
db45d..
address
TMMgd..
MetaCat_struct_p_product_constr