Proofgold Term Root Disambiguation

λ x0 x1 . Pi x1 (λ x2 . x0)

as obj
021ae..^setexp

as prop
-

theory
HotG

stx
08e38..

address
TMdMK..^setexp