Proofgold Term Root Disambiguation

∀ x0 x1 : ι → ι → ο . wceq (cesum x0 x1) (cuni (co (co cxrs (co cc0 cpnf cicc) cress) (cmpt x0 x1) ctsu))

as obj
-

as prop
c0524..

theory
SetMM

stx
2758d..

address
TMWVf..