Proofgold Term Root Disambiguation

λ x0 . and (struct_b_b_e_e x0) (unpack_b_b_e_e_o x0 (λ x1 . λ x2 x3 : ι → ι → ι . λ x4 x5 . explicit_Ring_with_id x1 x4 x5 x2 x3))

as obj
5b1d1..^Ring_with_id

as prop
-

theory
HotG

stx
ea380..

address
TMMXH..^Ring_with_id