Proofgold Term Root Disambiguation

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

as obj
-

as prop
9b221..^{explicit_Group_symgroup_inv_eq}

theory
HotG

stx
a0c68..

address
TMSEX..^{explicit_Group_symgroup_inv_eq}