Proofgold Term Root Disambiguation

λ x0 x1 . unpack_b_b_e_i x0 (λ x2 . λ x3 x4 : ι → ι → ι . λ x5 . explicit_Ring_minus x2 x5 x3 x4 x1)

as obj
c7259..^Ring_minus

as prop
-

theory
HotG

stx
ea380..

address
TMGB3..^Ring_minus