Proofgold Term Root Disambiguation

∀ x0 . x0 ∈ omega ⟶ SNoLev (eps_ x0) = ordsucc x0

as obj
-

as prop
75efd..^SNoLev_eps_

theory
HotG

stx
705e2..

address
TMdgB..^SNoLev_eps_