Proofgold Term Root Disambiguation

λ x0 . pack_b {x1 ∈ setexp x0 x0|bij x0 x0 (ap x1)} (λ x1 x2 . lam x0 (λ x3 . ap x2 (ap x1 x3)))

as obj
5a86a..^symgroup

as prop
-

theory
HotG

stx
a0c68..

address
TMZEL..^symgroup