Proofgold Term Root Disambiguation

λ x0 . {x1 ∈ SNoS_ (SNoLev x0)|SNoLt x1 x0}

as obj
48bcf..^SNoL

as prop
-

theory
HotG

stx
fab7c..

address
TMUvM..^SNoL