Proofgold Term Root Disambiguation

∀ x0 . setsum 0 x0 = Inj0 x0

as obj
-

as prop
b9c5c..^{Inj0_setsum_0L}

theory
HF

stx
a6670..

address
TMZR2..^{Inj0_setsum_0L}