Proofgold Term Root Disambiguation

λ x0 . λ x1 : ι → ι . prim3 (prim5 x0 x1)

as obj
24134..^famunion

as prop
-

theory
HotG

stx
18c18..

address
TMWQ7..^famunion