Proofgold Term Root Disambiguation

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

as obj
fe645..^{struct_b_quasigroup}

as prop
-

theory
HotG

stx
c1e43..

address
TMXYd..^{struct_b_quasigroup}