Proofgold Term Root Disambiguation

λ x0 x1 . pack_b {x2 ∈ setexp x0 x0|and (bij x0 x0 (ap x2)) (∀ x3 . x3 ∈ x1 ⟶ ap x2 x3 = x3)} (λ x2 x3 . lam x0 (λ x4 . ap x3 (ap x2 x4)))

as obj
3ec65..^{symgroup_fixing}

as prop
-

theory
HotG

stx
a0c68..

address
TMVDj..^{symgroup_fixing}