Proofgold Term Root Disambiguation

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

as obj
-

as prop
ac8dd..^SNoLtI2

theory
HF

stx
8964b..

address
TMbMJ..^SNoLtI2