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