Proofgold Term Root Disambiguation

λ x0 . prim0 (λ x1 . and (ordinal x1) (1beb9.. x1 x0))

as obj
e4431..

as prop
-

theory
HoTg

stx
38a69..

address
TMbTK..