Proofgold Term Root Disambiguation

λ x0 . setsum (ap x0 0) (ap x0 1) = x0

as obj
5c8a3..^pair_p

as prop
-

theory
HotG

stx
08e38..

address
TMSvX..^pair_p