Proofgold Term Root Disambiguation

λ x0 . unpack_b_b_e_e_i x0 (λ x1 . λ x2 x3 : ι → ι → ι . λ x4 x5 . pack_b_b_e x1 x2 x3 x4)

as obj
119ff..^{Ring_of_Ring_with_id}

as prop
-

theory
HotG

stx
ea380..

address
TMJ3J..^{Ring_of_Ring_with_id}