Proofgold Term Root Disambiguation

λ x0 . and (struct_b x0) (unpack_b_o x0 (λ x1 . λ x2 : ι → ι → ι . ∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ x2 (x2 x3 x4) x5 = x2 x3 (x2 x4 x5)))

as obj
a1c8b..^{struct_b_semigroup}

as prop
-

theory
HotG

stx
4cfdd..

address
TMW5s..^{struct_b_semigroup}