Proofgold Term Root Disambiguation

∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . subgroup (pack_b x0 x2) (pack_b x1 x3) ⟶ and (pack_b x0 x2 = pack_b x0 x3) (explicit_subgroup x1 x3 x0)

as obj
-

as prop
071cd..^{pack_b_subgroup_E}

theory
HotG

stx
a0c68..

address
TMUbU..^{pack_b_subgroup_E}