Proofgold Term Root Disambiguation

∀ x0 . ordinal x0 ⟶ (∀ x1 . x1 ∈ x0 ⟶ ordsucc x1 ∈ x0) ⟶ ∀ x1 . x1 ⊆ SNoS_ x0 ⟶ ∀ x2 . x2 ⊆ SNoS_ x0 ⟶ SNoCutP x1 x2 ⟶ SNoLev (SNoCut x1 x2) ∈ ordsucc x0

as obj
-

as prop
f1520..^{SNoCutP_SNoCut_lim}

theory
HotG

stx
9ae9f..

address
TMd6w..^{SNoCutP_SNoCut_lim}