Proofgold Term Root Disambiguation

∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . MetaCat x0 x1 x2 x3 ⟶ (∃ x4 x6 : ι → ι → ι → ι → ι . ∃ x8 : ι → ι → ι → ι → ι → ι → ι . MetaCat_coequalizer_buggy_struct_p x0 x1 x2 x3 x4 x6 x8) ⟶ (∃ x4 x6 x8 : ι → ι → ι . ∃ x10 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p x0 x1 x2 x3 x4 x6 x8 x10) ⟶ ∃ x4 x6 x8 : ι → ι → ι → ι → ι → ι . ∃ x10 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pushout_buggy_constr_p x0 x1 x2 x3 x4 x6 x8 x10

as obj
-

as prop
f0f28..

theory
HotG

stx
2772d..

address
TMcre..