Proofgold Term Root Disambiguation

λ x0 x1 . PNoLt (SNoLev x0) (λ x2 . x2 ∈ x0) (SNoLev x1) (λ x2 . x2 ∈ x1)

as obj
8c8aa..^SNoLt

as prop
-

theory
HotG

stx
fab7c..

address
TMQeB..^SNoLt