Proofgold Term Root Disambiguation

∀ x0 x1 x2 . In x2 (Pi x0 (λ x3 . x1)) ⟶ In x2 (setexp x1 x0)

as obj
-

as prop
4322e..^setexp_I

theory
HF

stx
b6147..

address
TMG6S..^setexp_I