Proofgold Term Root Disambiguation

λ x0 . Sep (SNoS_ (SNoLev x0)) (SNoLt x0)

as obj
0cfe8..^SNoR

as prop
-

theory
HotG

stx
fab7c..

address
TMSvK..^SNoR