Proofgold Term Root Disambiguation

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

as obj
-

as prop
a11cf..^{mordinal_SNoLev_min}

theory
HotG

stx
2cf07..

address
TMGx6..^{mordinal_SNoLev_min}