Proofgold Term Root Disambiguation

∀ x0 : ι → ο . w3a (wcel x0 ceven) (wbr c4 x0 clt) (wbr x0 (co c4 (co (cdc c1 cc0) (cdc c1 c8) cexp) cmul) cle) ⟶ wcel x0 cgbe

as obj
-

as prop
e3037..

theory
SetMM

stx
d0f6d..

address
TMHin..