Proofgold Term Root Disambiguation

∀ x0 x1 . ap (setsum x0 x1) 1 = x1

as obj
-

as prop
cce3d..^pair_ap_1

theory
HotG

stx
08e38..

address
TMSs4..^pair_ap_1