Proofgold Term Root Disambiguation

∀ x0 x1 x2 . In x2 (setexp x1 x0) ⟶ lam x0 (ap x2) = x2

as obj
-

as prop
09a68..^setexp_eta

theory
HF

stx
b2d3f..

address
TMJ8i..^setexp_eta