Proofgold Term Root Disambiguation

λ x0 x1 . ReplSep x0 (λ x2 . ∃ x3 . x2 = setsum x1 x3) proj1

as obj
a4d82..^ap

as prop
-

theory
HotG

stx
08e38..

address
TMRkK..^ap