Proofgold Term Root Disambiguation

∀ x0 x1 . In x1 (proj0 x0) ⟶ In (setsum 0 x1) x0

as obj
-

as prop
88f5c..^proj0E

theory
HF

stx
cbc45..

address
TMSSF..^proj0E