Proofgold Term Root Disambiguation

∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . (∀ x8 : ο . (∀ x9 : ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι . (∀ x12 : ο . (∀ x13 : ι → ι → ι → ι → ι . MetaCat_exp_constr_p PER BinRelnHom struct_id struct_comp x1 x3 x5 x7 x9 x11 x13 ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0

as obj
-

as prop
97ee8..^{MetaCat_struct_r_per_product_exponent}

theory
HotG

stx
7b0f2..

address
TMcVY..^{MetaCat_struct_r_per_product_exponent}