Proofgold Term Root Disambiguation

In_rec_i (λ x0 . λ x1 : ι → ι . binunion (Sing 0) (prim5 x0 x1))

as obj
7736c..^Inj1

as prop
-

theory
HotG

stx
114a5..

address
TMHfH..^Inj1