Proofgold Term Root Disambiguation

λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 : ι → ι → ι . λ x7 : ι → ι → ι → ι → ι → ι . λ x8 x9 : ι → ι → ι . λ x10 : ι → ι → ι → ι → ι . and (MetaCat_product_constr_p x0 x1 x2 x3 x4 x5 x6 x7) (∀ x11 x12 . x0 x11 ⟶ x0 x12 ⟶ MetaCat_exp_p x0 x1 x2 x3 x4 x5 x6 x7 x11 x12 (x8 x11 x12) (x9 x11 x12) (x10 x11 x12))

as obj
fbdca..^{product_exponent_constr_p}

as prop
-

theory
HotG

stx
2772d..

address
TMX1y..^{product_exponent_constr_p}