Proofgold Term Root Disambiguation

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

as obj
-

as prop
9bbf1..^{explicit_subgroup_symgroup_fixing}

theory
HotG

stx
a0c68..

address
TMWhK..^{explicit_subgroup_symgroup_fixing}