Proofgold Term Root Disambiguation

∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . Group (pack_b x0 x1) ⟶ x2 ⊆ x0 ⟶ explicit_Group_identity x0 x1 ∈ x2 ⟶ (∀ x3 . x3 ∈ x2 ⟶ explicit_Group_inverse x0 x1 x3 ∈ x2) ⟶ (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ x1 x3 x4 ∈ x2) ⟶ explicit_subgroup x0 x1 x2

as obj
-

as prop
febae..^{explicit_subgroup_test}

theory
HotG

stx
a0c68..

address
TMF72..^{explicit_subgroup_test}