Proofgold Term Root Disambiguation

∀ x0 x1 . In x1 (proj1 x0) ⟶ In (setsum 1 x1) x0

as obj
-

as prop
13e9e..^proj1E

theory
HF

stx
cbc45..

address
TMTff..^proj1E