Proofgold Term Root Disambiguation

λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . and (and (and (MetaFunctor_prop1 x0 x1 x2 x3) (MetaFunctor_prop2 x0 x1 x2 x3)) (and (MetaCat_IdR_p x0 x1 x2 x3) (MetaCat_IdL_p x0 x1 x2 x3))) (MetaCat_Comp_assoc_p x0 x1 x2 x3)

as obj
1fb9a..^MetaCat

as prop
-

theory
HotG

stx
2772d..

address
TMYMZ..^MetaCat