Proofgold Term Root Disambiguation

λ x0 x1 . ReplSep x0 (λ x2 . ∀ x3 : ο . (∀ x4 . x2 = setsum x1 x4 ⟶ x3) ⟶ x3) proj1

as obj
a4d82..^ap

as prop
-

theory
HotG

stx
08e38..

address
TMRkK..^ap