Proofgold Term Root Disambiguation

∀ x0 x1 . SNoLev x0 ∈ SNoLev x1 ⟶ SNoEq_ (SNoLev x0) x0 x1 ⟶ SNoLev x0 ∈ x1 ⟶ SNoLt x0 x1

as obj
-

as prop
82b82..^SNoLtI2

theory
HotG

stx
fab7c..

address
TMSSV..^SNoLtI2