Proofgold Term Root Disambiguation

In_rec_i (λ x0 . λ x1 : ι → ι . famunion x0 (λ x2 . prim4 (x1 x2)))

as obj
1ce9f..

as prop
-

theory
HotG

stx
f4683..

address
TMUTi..