Proofgold Term Root Disambiguation

∀ x0 x1 x2 : ι → ο . w3a (wcel x0 chil) (wcel x1 chil) (wcel x2 chil) ⟶ wceq (co (co x0 x1 cva) x2 csp) (co (co x0 x2 csp) (co x1 x2 csp) caddc)

as obj
-

as prop
efb84..

theory
SetMM

stx
47223..

address
TMXTB..