Proofgold Term Root Disambiguation

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

as obj
-

as prop
2004d..^{explicit_Group_symgroup}

theory
HotG

stx
a0c68..

address
TMKpf..^{explicit_Group_symgroup}