Proofgold Term Root Disambiguation

λ x0 . and (TransSet x0) (∀ x1 . prim1 x1 x0 ⟶ TransSet x1)

as obj
f4851..

as prop
-

theory
HoTg

stx
c93a1..

address
TMMUu..^ordinal