Proofgold Term Root Disambiguation

∀ x0 . explicit_Group_identity {x2 ∈ setexp x0 x0|bij x0 x0 (ap x2)} (λ x2 x3 . lam x0 (λ x4 . ap x3 (ap x2 x4))) = lam x0 (λ x2 . x2)

as obj
-

as prop
fce19..^{explicit_Group_symgroup_id_eq}

theory
HotG

stx
a0c68..

address
TMZFo..^{explicit_Group_symgroup_id_eq}