Proofgold Term Root Disambiguation

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

as obj
-

as prop
94072..^SNoLtI3

theory
HF

stx
8964b..

address
TMZcu..^SNoLtI3