Proofgold Term Root Disambiguation

∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 . MagmaHom (pack_b x0 x2) (pack_b x1 x3) x4 = and (x4 ∈ setexp x1 x0) (∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ap x4 (x2 x6 x7) = x3 (ap x4 x6) (ap x4 x7))

as obj
-

as prop
2cd8d..^{Hom_struct_b_pack}

theory
HotG

stx
820be..

address
TMXCM..^{Hom_struct_b_pack}