Proofgold Term Root Disambiguation

λ x0 x1 x2 . and (Group_Hom x0 x1 x2) (bij (field0 x0) (field0 x1) (ap x2))

as obj
35784..^Group_Iso

as prop
-

theory
HotG

stx
6b5ba..

address
TMNoS..^Group_Iso