Proofgold Term Root Disambiguation

∀ x0 . ordinal x0 ⟶ ∀ x1 . SNo x1 ⟶ SNoLev x1 ∈ ordsucc x0 ⟶ SNoLe (minus_SNo x0) x1

as obj
-

as prop
a96d6..^{mordinal_SNoLev_min_2}

theory
HotG

stx
2cf07..

address
TMdLN..^{mordinal_SNoLev_min_2}