Proofgold Proposition

∃ x0 x2 x4 : ι → ι → ι . ∃ x6 : ι → ι → ι → ι → ι → ι . ∃ x8 x10 : ι → ι → ι . ∃ x12 : ι → ι → ι → ι → ι . MetaCat_exp_constr_p (λ x14 . x14 ∈ prim6 0) HomSet lam_id (λ x14 x15 x16 . lam_comp x14) x0 x2 x4 x6 x8 x10 x12

type
prop

theory
HotG

name
-

proof
PUQ8q..

Megalodon
MetaCatHFSet_product_exponent

proofgold address
TMdmR..^{MetaCatHFSet_product_exponent}

creator
11511 PrEBh../73033..

owner
11520 PrEBh../de220..

term root
b7e68..