Proofgold Term Root Disambiguation

λ x0 . λ x1 : ι → ι . famunion x0 (λ x2 . prim5 (x1 x2) (setsum x2))

as obj
d64bc..^Sigma

as prop
-

theory
HotG

stx
08e38..

address
TMMDL..^Sigma