Proofgold Term Root Disambiguation

∀ x0 . ordinal x0 ⟶ ∀ x1 . x1 ∈ SNoS_ x0 ⟶ ∀ x2 : ο . (SNoLev x1 ∈ x0 ⟶ ordinal (SNoLev x1) ⟶ SNo x1 ⟶ SNo_ (SNoLev x1) x1 ⟶ x2) ⟶ x2

as obj
-

as prop
62b49..^SNoS_E2

theory
HotG

stx
fab7c..

address
TMRab..^SNoS_E2